Reasoning-chain verification
Each lemma, proposition and its dependency edges are formalized and discharged by the Lean kernel.
LeanNexus formalizes research mathematics into machine-checked, Lean-based proofs — verifying every reasoning step, re-deriving every computation, and localizing the exact line where an argument breaks.
Producing advanced and verifiable mathematical data.
Formalizing research mathematics is possible by domain experts, but it is slow, specialized, and difficult to scale. LeanNexus turns domain expertise into Lean automation to structure arguments, verify dependencies, re-derive key computations, and preserve the results as machine-checkable mathematical knowledge.
Each lemma, proposition and its dependency edges are formalized and discharged by the Lean kernel.
Constants, bounds and closed forms are re-computed from first principles with interval arithmetic and certified numerics.
When a step goes wrong, we report the failing goal, the missing hypothesis, and where possible a concrete counterexample.
The output is not a report — it is a Lean repository plus an auditable dependency graph that anyone can re-check for their own purposes.
Upload a LaTeX project, point at an arXiv ID, or drop a single source file. Figures, .sty and .bib come along; version-control metadata is stripped.
The paper is decomposed into statements, definitions, and dependencies, then formalized in Lean against Mathlib. Every accepted step is checked by the Lean kernel.
The output includes an interactive checkpoint graph, a Lean repository that builds from scratch, a structured categorization of each proof step, and clear recommendations for improving the argument.
Select any node to trace a claim from the paper to its Lean statement, proof dependencies, and kernel status. The graph reveals what has been verified, what remains open, and exactly where a proof fails.
Formal statement matches the prose claim, adjudicated by an independent reviewer.
Median wall-clock against a trained formalizer on the same paper.
Submission to first complete checkpoint graph, mid-length paper.
No step is accepted on a model's say-so. The Lean kernel is the only authority.
Figures are placeholder — replace with the benchmark table your team signs off on.
Start with one consequential section. We will return a verification graph, a Lean repository, and an honest list of what we could not close.