Axiomatic AI Open lemma
at a glance

We verify and validate.

An AI workspace for research. Made by scientists and engineers, for scientists and engineers.

Who builds it

Scientists and engineers

Built by physicists and engineers who use it for their own research, and tuned for science and engineering, not general chat.

What sets it apart

Verification and validation

Equations, numbers, claims and references are checked, and you see how each check was done.

How you work

A real workspace

A sandbox where your computations run, and where long jobs keep running in the background.

  • Standard1 CPU · 4 GB
  • High performance20 CPUs · 64 GB
  • GPUNVIDIA H200 · 20 CPUs · 192 GB
What's installed

Installed packages and tools

Suitable for co-design: combine tools in one notebook, such as Optiland ray optics with Tidy3D FDTD.

Tidy3DMEEPOptilandgdsfactoryQuTiPQiskitDEVSIMPySpicepymatgenJAXPyTorchSymPySciPymarimoPlotlyLean 4Z3LaTeXJulia
92 Python packages pre-installed, plus Julia, LaTeX, Lean, MEEP, ngspice and aestimo
Overview

Checked results, in a real workspace.

Frontier AI tools used out of the box miss many of the errors in scientific work. Lemma checks the science, the numbers and the sources, and runs the code, simulations and documents in a workspace you control.

Verification & validation

Trust, but check.

  • ✓
    Verification modePlan & verify: Lemma plans the work, runs every task with its own checks and hands you a verification & validation report.
  • ✓
    Verify the scienceDerivations, equations and numerical claims are recomputed in code, not just read.
  • ✓
    Validate against sourcesEvery reference is checked for existence, correctness and relevance. Results are compared with the published figures.
  • ✓
    Formal checks with LeanKey results can be proved formally, and Lean checks the numbers in the background.
  • ✓
    Reasoning you can auditEvery step as code, plots and an annotated PDF, so you can rerun it and judge it yourself.
watch the full run
1 in 3
recent arXiv preprints has at least one error in its references
~50%
of known errors in a paper can be missed by standard AI models
From our paper-validation benchmark →

Axiomatic Knowledge Base

Connected to a curated knowledge graph of scientific papers.

Interactive graphics

Live notebooks with sliders, 3D views and animations. The results are models you can play with, not static images.

LaTeX editing and compiling

Write and edit your manuscript with Lemma, and compile it to PDF in the same workspace.

\begin{equation}
  E = \hbar v_F |k|
\end{equation}
Coming soon

Open-weight models

Run Lemma on open-weight models for extra data protection.

Examples

01 · Validate a paper

Checking every reference and equation by hand takes days. lemma checks them all.

Errors slip through review: 1 in 3 recent arXiv preprints has at least one error in its references. Attach a PDF and lemma checks its references, claims and equations, and marks each issue where it occurs.

watch the full run
01

Validate a paper

Check a paper's references, claims and equations.

Returns an annotated PDF with each issue marked where it occurs
The result
An annotated PDF, every issue marked in place
What it checks
  • ReferencesEach one checked for existence, correctness and relevance.
  • Claims and equationsRecomputed in code, not just read.
  • A verdict per claimWith its caveats, when a claim only holds under assumptions.
  • Code you can rerunEach note points to the script that checked it.
02 · Co-design

Real devices span scales no single simulator covers. Co-design combines the tools.

A lens system lives in millimetres, a grating coupler in nanometres, and each needs its own solver. lemma combines multiple tools to solve one problem: here Optiland for the optics and Tidy3D for the chip, in one notebook.

watch the full run
02

Co-design with multiple tools

Real solvers, such as Optiland, Tidy3D, QuTiP, Qiskit and DEVSIM, combined in one notebook.

Quick result, or a validated study with convergence checks
The result
36% of the light reaches the waveguide
What it built
  • OptilandA beam expander and focusing lens, with its traced rays.
  • Tidy3DThe grating coupler, phase-matched at 1550 nm, lit by the beam from Optiland.
  • A hand-off between toolsOptiland → bridge → Tidy3D → overlap, from millimetres to nanometres.
  • One parameter, both solversChange the design and both beams shift and spread together.
03 · Make a paper interactive

A paper is static: you can't change a parameter and see what happens. lemma makes it interactive.

lemma reads the paper and rebuilds its optical system as a live model you can change, checked against the paper's claims.

watch the full run
03

Make a paper interactive

Easier reading: watch a paper's physics come to life.

The model is rebuilt from the paper and checked against its claims
The result
The paper's Fig. 3, reproduced by ray tracing
The notebook it built
  • The whole system in 3DFour lenses, the vacuum window and the focus.
  • Change itWiden one air gap by 1 mm: focal length and image quality leave the paper's values.
  • ResetBack to the paper's values, and every claim reproduces again.
04 · Digital twin of a paper

Reproducing a paper's results by hand is slow. lemma rebuilds them, live.

Here: a lithography metrology paper (Messinis et al., Optics Express 2021). lemma rebuilds the microscope lens in Optiland and the wafer targets in Tidy3D.

watch the full run
04

Digital twin of a paper

Reproduce a paper's figures live, next to the original.

Side-by-side comparison with the published figures
The result
The paper's Fig. 6(b), reproduced
The notebook it built
  • The lensThe Thorlabs A240, ray traced in Optiland.
  • The targetsAn 80 nm gold calibration cube and an overlay grating on silicon, in Tidy3D.
  • Near field through the lensFDTD images, raw and aberration-corrected, as in Fig. 7.
  • Defocus the sampleThe raw image falls apart, the correction holds. Reset returns to the paper.
05 · Teach me a topic

Getting into a new field means weeks of reading. lemma teaches it at your level.

Ask how superconductivity can come from repulsion. lemma reads the literature, writes a short, visual, interactive lesson and checks its physics.

watch the full run
05

Teach me a topic

A short, visual, interactive lesson at your level.

Grounded in the literature, with the sources cited
The check
19 of 20 physics checks pass, none fail
The lesson it built
  • Grounded in four papersRead and cited in the lesson.
  • Live physicsRepulsive interactions and d-wave pairing, animated.
  • ValidatedOne click runs the physics checks and lists the results in a table.
06 · Survey the literature

There are too many papers to read them all. lemma finds and compares the key ones.

lemma finds, reads and compares the key papers on a topic, in an interactive notebook.

watch the full run
06

Survey the literature

Find, read and compare the key papers on a topic.

Every source linked, with a ready-to-use BibTeX file
You get
Every source linked, plus a BibTeX file
In the notebook
  • Found and readThe key papers on your topic, each one linked.
  • ComparedSide by side, in an interactive notebook.
07 · Extract data from a figure

The data you need is often locked inside a plot. lemma turns it into numbers.

lemma digitises a plot into an interactive notebook, then optionally fits a model.

watch the full run
07

Extract data from a figure

Digitise a plot, then optionally fit a model.

The extracted data is replotted next to the original, so you can check the match
You get
The data, replotted next to the original
In the notebook
  • DigitisedThe curves of the figure as numbers you can use.
  • Fit a modelOptionally, fitted in the same notebook.
08 · Try an example

Starting a model from scratch is slow. Start from a working notebook.

Open a ready-made twisted-bilayer-graphene notebook, then ask for something similar: bilayer graphene on hBN.

watch the full run
08

Try an example

Open a working notebook, play with the physics, then make it your own.

From twisted bilayer graphene to bilayer graphene on hBN in one session
The result
A new moiré model, built and checked
The notebook it built
  • A new notebookBilayer graphene on hBN, from the twisted-bilayer starting point.
  • Band structureThe moiré minibands, checked against the literature.
  • In 3DThree layers, atom by atom: the moiré from twist and lattice mismatch.
  • LiveTurn up the displacement field and the minibands reshape.
09 · Solve a problem set

Knowing the answer is not the same as understanding it. lemma builds the lesson around it.

Attach a screenshot of a hard problem. lemma solves it, checks the result numerically and builds a notebook you can play with to understand why.

watch the full run
09

Solve a problem set

Attach a screenshot of a hard problem. Here: Kapitza's pendulum, a pendulum that balances upside down on a vibrating pivot.

Each part answered, then checked against the full equation of motion
The answer
Stable if a²Ω² > 2gℓ, so fmin ≈ 31.5 Hz
The notebook it built
  • Every step derivedFrom the Lagrangian to the effective potential and the small-oscillation frequency.
  • SlidersDrag Ω past the threshold and watch the hilltop at θ = 0 turn into a well.
  • The full equation, animatedNo averaging: the pendulum falls below threshold and stays up above it.
  • CheckedA Floquet analysis of the exact equation gives the same threshold to 0.05%, and the notebook states what it did not check.
Get started

Bring a paper, a question or a device.
Lemma checks the rest.

Made by scientists and engineers, for scientists and engineers.

Try lemma Read the benchmark