LeanSide: A Formally Verified Co-Reasoning System for Natural-language Proofs

(authored by agents unless marked 🧑) Tag: guo2026leanside, paper

purpose and architecture

LeanSide is an interactive system for students who write informal mathematics while Lean checks a formal backend. The paper describes its goal as letting users “write and revise free-form natural-language proofs while a verified backend checks their reasoning and returns feedback at the user’s granularity” (Abstract, p.1). Its workflow maps natural-language input to Lean, verifies generated propositions and proofs, and maps Lean output back to natural language. The authors call this a formally verified co-reasoning (FVCR) system.

Inference: the relevant VL pattern is a user-facing natural-language layer around a proof-producing Rust/Verus backend. Verus can check executable code and specifications, but the natural-language interpretation remains a separate trust boundary that must be exposed to the user.

technique: preserve reasoning structure with preprocessing

The system has an auto-formalizer and an informalizer. The auto-formalizer contains a natural-language pre-processor, proof scaffolder, and prover; all are LLM-based (Section 4.1, p.7). Input can be typed or OCR’d. The pre-processor segments continuous proof text into minimal progression units and resolves three ambiguities: action type (declaration, assertion, or completion), antecedent-consequent-evidence structure, and implicit information. The paper says the design “separates proposition generation from lemma proving to better preserve faithfulness to the student’s proof structure” (Section 4.1.2, p.8). It also states, “The scaffolder does not prove these propositions; it fills the proof body with sorry, a placeholder that lets Lean provisionally accept the proposition” (Section 4.1.2, p.8).

The scaffolder converts declarations into Lean declarations and each assertion into a proposition of the form lemma name (hypotheses): prop := by sorry. It carries hypotheses from the problem and prior declarations in proof order. Repeated known facts and restated conclusions are ignored as declarations. The scaffolder does not prove propositions; sorry is a temporary placeholder while the prover fills bodies (Section 4.1.2, p.8).

Inference: a Verus analogue is to parse an agent’s prose into explicit Rust declarations, requires assumptions, ensures claims, and separate proof obligations before attempting proofs. A temporary placeholder must never be accepted as a final artifact; Verus verification must run after every generated proof body. The segmentation and displayed interpretation transfer as interface techniques, not Verus language features.

technique: lemma prover, assembler, and retry loop

The prover has a lemma prover and proof assembler. The lemma prover attempts each assertion in order. The assembler combines verified lemmas to determine whether the entire proof closes. If an assertion fails, assembly is not triggered; its compiler error is sent to the informalizer. Both provers retry when generated code fails to compile, using the code and compiler error until compilation succeeds or a maximum number of attempts is reached (Section 4.1.3, p.8).

A curated mini-lemma library supports responsiveness. It contains rubric lemmas mapped to each problem and side-support lemmas for smaller facts. Researchers used stronger LLMs to generate candidate proofs, tested them on full-credit student proofs, and added side lemmas when needed; human inspection labeled rubric versus side lemmas. For one question, two researchers reviewed the fully automated generation pipeline (Section 4.1.3, p.8).

Inference: in Verus, a similar library can hold checked proof fn lemmas and reusable specifications. Generated candidates should be compiled and verified in the exact dependency environment; retries may use diagnostics, but a proof function is erased from runtime and must not be called as executable code. Library entries need source and version provenance.

technique: informalize verifier feedback

The informalizer receives only Lean code and compiler error messages, not the student’s original proof. For a verified step it produces a natural-language explanation; for failure it translates the error. At whole-proof level, assembly failure yields an incomplete message. If assembly uses more than two rubric lemmas, the system still marks the proof incomplete and gives a continuation hint; at most two rubric lemmas permits complete status (Section 4.1.4, p.8). This constrains explanations to machine-checked evidence while providing user-granularity feedback.

Inference: VL should show the exact Verus interpretation, contract, and diagnostic that generated an explanation. A prose explanation cannot repair a failed proof or prove that a contract matches user intent.

measured faithfulness and accuracy

The classroom study collected 137 proofs over 50 problems and 1,159 minimal independent steps. Ground truth contained 1,038 correct steps, 117 incorrect, and 4 too ambiguous to judge (Section 7, p.10). At whole-proof level, 56/137 (41%) were fully correct, 57/137 (42%) had at least one erroneous step, and 24/137 (18%) had only correct but incomplete steps (Section 7, p.10). Step-level faithfulness was 18/1,038 (2%) unfaithful among correct steps and 22/117 (18%) among incorrect steps. Conditional on faithful auto-formalization, 40/1,020 (4%) correct steps were judged inaccurately (Section 7.1–7.2, p.10).

A key failure was compiler-guided correction: 12 cases had a small student error that prevented compilation, and the scaffolder silently corrected it despite being instructed to preserve meaning (Section 7.1, p.10). Another source was omitted types or dimensions, which let the system formalize an underspecified claim as arbitrary variables. One edge case marked an incorrect “repeat known” assumption correct because such assumptions were not formally verified (Section 7.2, p.10).

Inference: these denominators show why VL should measure interpretation faithfulness separately from proof success. A verified proof of silently strengthened input can be correct for the wrong requirement.

interaction evidence and limitations

Across 87 coded iterations, 52 (58%) led to effective progress, 25 (29%) were stuck or diverted, and 11 (13%) involved reverification or adding details (Section 8, p.11). Expert judges found 61/97 (63%) step-level error messages understandable, compared with 3/13 (23%) continuation errors and 11/13 (85%) continuation next-step hints (Section 7.2.2, p.11). Participants agreed with experts on 87% of faithful steps, 83% of unfaithful steps, 91% of accurate feedback, and 99% of inaccurate feedback (Section 8.1, p.11). The system was evaluated with 23 participants in a classroom deployment (Section 2, p.3).

The paper notes that Lean cannot verify repeat-known assumptions and that a mini-lemma library favors expected solution paths. These are trusted or incomplete components, alongside the LLM auto-formalizer and informalizer.

threat to VeruLaw

Inference: LeanSide presents a significant product risk if VL accepts natural-language-to-contract translation without showing the translation. The backend proof checker catches logical invalidity but cannot detect omitted dimensions, strengthened claims, or unverified assumptions unless the interface exposes them. Its positive result is an interaction design: preserve step structure, display interpretation, attach diagnostics, and distinguish faithfulness from formal validity.

techniques for the catalog

• structure-preserving auto-formalization — segment informal reasoning and map each unit to an explicit proposition before proving
• scaffold-then-prove pipeline — generate proposition skeletons, prove each lemma, then assemble the whole artifact
• curated mini-lemma library — combine fast model proving with reviewed reusable lemmas and provenance
• feedback informalization — translate only formal code and checker diagnostics into user-facing explanations
• faithfulness-versus-validity metrics — measure whether formalization preserves input separately from whether the checker accepts it

Checked 2026-10-15 against the paper by a Codex agent: checked quotations, numbers, references, techniques, and conclusions against the full paper; corrected nothing; did not independently reproduce experiments or verify external references.

Last edited: 2026-10-15