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

1 Introduction

• Prior auto-formalization mainly targets verified code for advanced problems, not faithful support for ambiguous, incomplete, or evolving user reasoning.Most systems inherit a post-hoc model centered on finished, textbook-style proofs.Source: §1 · pp. 1–2
• LeanSide pairs familiar-language proof input and revision with a verified backend that formalizes reasoning and translates verification output into everyday language.The interaction is designed to help users assess both whether their reasoning was understood and what the verifier concluded.Source: §1 · p. 2, Figure 1 · p. 2
• The study examines this approach in undergraduate mathematics, where students use LLM tools despite risks of incorrect answers and redirection from their reasoning paths.LeanSide supports students expressing reasoning at their chosen level of detail and iterating on proof mistakes, without aiming to act as a tutor.Source: §1 · p. 2
• The paper contributes the LeanSide system, a 23-participant user study alongside classroom deployment, and findings on progress barriers and design implications.The study focuses on whether and how students use system feedback to iterate on proofs.Source: §1 · p. 2

2.1 Challenges of human-AI collaboration in reasoning tasks

• LLM reasoning can produce errors that users may miss, while plausible misalignment can undermine agency; prior interfaces expose inconsistencies or interpretations, motivating inspectable system understanding.LeanSide instead uses a formally verified backend to reduce hallucinations.Source: §2.1 · pp. 2–3

2.2 Lean and auto-formalization

• Interactive theorem provers offer machine-checked mathematics but remain difficult for non-experts because of their learning curve and fine-grained reasoning demands.Auto-formalization addresses this accessibility gap through theorem translation and proof generation.Source: §2.2 · p. 3
• Many benchmarks assume polished, one-shot inputs, whereas student proofs are often fragmented and iterative; this motivates studying auto-formalization as co-reasoning.Several datasets also derive from formal corpora rather than situated human proof writing.Source: §2.2 · p. 3

2.3 Making formal verification accessible

• Prior accessibility approaches include classroom instruction, visualizations, controlled language, and expert-facing formalization tools, but each has limitations in feedback or supported utterances.Formal verification beyond mathematics has often emphasized technical realization over how people use informal-language feedback.Source: §2.3 · pp. 3–4
• LeanSide moves beyond expert-facing tools by combining a natural-language interface with study of how people interact with formally verified feedback in practice.Source: §2.3 · p. 4

3 System design

• The design targets undergraduate students without Lean knowledge and supports natural-language expression, proof validation, and iteration through expressiveness, accessible feedback, and transparency.The workflow accepts typed or handwritten reasoning, returns informalized verification feedback, and lets users revise without reading or writing Lean.Source: §3 · p. 4

3.1 Expressiveness via wide walls

• Students can type or upload handwritten proofs, including ambiguous, exploratory, incorrect, or incomplete work, rather than only polished textbook-style proofs.These input modes are intended to support the varied forms and granularity in which students naturally write proofs.Source: §3.1 · p. 4

3.2 Low Threshold and High Ceiling

• Step-level displays map written steps to informalized Lean interpretations, marking verified assertions green and failed assertions yellow with errors.The interface also provides continuation messages or hints for incomplete proofs, large-jump warnings, optional suggestions, and access to Lean code.Source: §3.2 · p. 4

3.3 Transparency

• Transparency lets users inspect whether formalization matches their intended reasoning and view how the system resolves ambiguous references and classifies sentences.Source: §3.3 · p. 4

4 Implementation

• Implementation requirements include interpreting incorrect, ambiguous, or incomplete reasoning, preserving the student’s path, judging course-level validity, and returning timely feedback.A formally valid step can still be unacceptable in context if it skips an instructor-defined intermediate step.Source: §4 · pp. 4–5

4.1 System pipeline

• The pipeline auto-formalizes input through preprocessing, scaffolding, and proving, then informalizes generated Lean code and errors for students.A mini-lemma library supports the lemma prover.Source: §4.1 · p. 5, Figure 4 · p. 6

4.1.1 Natural-language pre-processor.

• The pre-processor resolves referential, action-type, and antecedent-consequent-evidence ambiguity, then segments assertions into minimal progression units.Each unit is a self-contained statement with an antecedent, consequent, and evidence, at the level of content expressed by the student.Source: §4.1.1 · p. 5

4.1.2 Proof Scaffolder.

• The scaffolder maps progression units to Lean lemmas: declarations become code where appropriate, while assertions become propositions with proof bodies left as sorry.This separates proposition generation from proving to preserve the student’s proof structure.Source: §4.1.2 · pp. 5–6

4.1.3 Prover.

• The prover checks assertion lemmas in student order, assembles verified lemmas into a whole proof, and retries compile failures using compiler errors.A curated library of rubric and side-support lemmas supplements faster prover models; its development includes testing against full-credit exam proofs.Source: §4.1.3 · p. 6

4.1.4 Informalizer.

• The informalizer turns Lean propositions and compiler errors into course-aligned natural-language feedback without seeing the student’s proof.Step feedback marks verified claims or explains failures; whole-proof feedback distinguishes incomplete proofs from complete ones based on assembly and rubric lemmas.Source: §4.1.4 · pp. 6–7

5.1 Context: classroom deployment

• The system was deployed for 13 weeks in an advanced undergraduate linear algebra course, with 14 questions released during the semester.Most students were computer science majors; the team conducted three pilots before deployment.Source: §5.1 · p. 7

5.2 Participants

• The analysis covered 23 usable sessions from 27 conducted; 22 participants had previously used the system, but none could independently write a Lean proof.Fourteen of the 23 participants were computer science majors, and 21 were undergraduates.Source: §5.2 · p. 7

5.3 One-on-one User study protocol

• In two-hour sessions, students spent 90 minutes writing and revising proofs with system feedback, followed by a brief interview.They chose questions they had not previously attempted with the system and were encouraged to select uncertain problems; AI tools were not allowed.Source: §5.3 · p. 7

5.4 Analysis and Evaluation

• Researchers assessed expert-rated system performance, perceived performance, proof progress, student comments, and interview responses.Two course-familiar researchers independently judged 20% of sessions, with instructor resolution of disagreements; thematic analysis guided coding of comments and interviews.Source: §5.4 · pp. 7–8
• Figure 5 presents an example of a student iterating on one problem from beginning to end.The caption identifies it as a usage example of the workflow.Source: Figure 5 · p. 8

• P2 began without a clear strategy and entered tentative steps, including repeated hypotheses and familiar facts.The first system error was confusing and unhelpful, so P2 searched the browser for guidance and rewrote the proof on paper.Source: §6 · p. 8
• After revising, P2 judged later feedback accurate and corrected a step, eventually verifying every step.The trajectory included both unhelpful and helpful feedback.Source: §6 · p. 8
• Before submitting, P2 checked whether each system interpretation matched his intent.After checking every step, he submitted the assignment.Source: §6 · p. 8

7 Prerequisites for natural-language access to verification

• Of 137 proofs, 56 (41%) were fully correct, 57 (42%) contained an error, and 24 (18%) were correct but incomplete; 11/56 (20%) and 4/56 (7%) fully correct proofs were flagged erroneous or incomplete.Figure 6 separates whole-proof results on the left from step-level results on the right.Source: §7 · p. 8, Figure 6 · p. 9

7.1 System performance on faithfulness

• 18/1038 (2%) correct steps and 22/117 (18%) incorrect steps were judged unfaithful.Most unfaithfulness arose during auto-formalization; three cases involved both auto-formalization and informalization, and one involved informalization alone.Source: §7.1 · p. 9
• Small formal errors could trigger compiler-guided correction during auto-formalization, while vague or ambiguous steps could be formalized as stronger claims inconsistent with students’ intended meaning.The small-error pattern occurred in 12 cases; it was the pipeline’s most likely source of unfaithful autocorrection.Source: §7.1 · p. 9

7.2.1 Step-wise accuracy.

• 40/1020 (4%) faithful correct steps were judged wrong; steps more granular than a rubric item counted as incorrect even when mathematically valid.Source: §7.2.1 · p. 9
• The prover sometimes failed on valid steps outside its expected solution paths, while omitted variable types or dimensions could lead the scaffolder to formalize variables incorrectly.The mini-lemma library was built around expected strategies, and the prover prioritized responsiveness over proving arbitrary propositions.Source: §7.2.1 · pp. 9–10

7.2.2 Error-message understandability.

• 61/97 (63%) step-level error messages, 3/13 (23%) continuation error messages, and 11/13 (85%) continuation next-step hints accurately reflected what was wrong or needed next.Source: §7.2.2 · p. 10
• Step-level errors were often too granular for students’ assertions, while continuation errors could miss user granularity; next-step hints were more understandable because they followed course-context rubric items.Source: §7.2.2 · p. 10

8.1 Could participants assess the system’s accuracy and faithfulness?

• Participants matched experts on 87% of faithful and 83% of unfaithful steps, and 91% of accurate and 99% of inaccurate feedback; they judged faithfulness by mathematical equivalence.Informalizations often looked different from students’ inputs even when faithful, so this judgment required mathematical knowledge.Source: §8.1 · p. 10, §8.1.2 · pp. 10–11

8.1.1 How do participants judge a claim as inaccurate?

• Students judged local errors using mathematical context, but inaccurate messages led them to reverify, add detail, or stop when they trusted their own claim.Lean could fail on claims students found easy when a needed theorem was unavailable or an informal claim required a non-trivial formal proof.Source: §8.1.1 · p. 10

8 User study findings

• 52 of 87 iterations (58%) led to progress, 25 (29%) were unhelpful or involved getting stuck or diversion, and 11 (13%) involved reverification or added detail.Figure 7 reports the distribution of coded revision outcomes.Source: §8 · p. 10, Figure 7 · p. 11

8.2.1 Progress type 1: Repairing proofs with accurate, understand-

• Accurate, understandable step feedback exposed overlooked constraints and helped turn tentative conceptual ideas into more rigorous proofs.Predicted interpretations, including ambiguity labels, helped students identify where their intent had or had not been captured.Source: §8.2.1 · p. 11, §8.2.2 · pp. 11–12

8.2.3 Progress type 3: Advancing with continuation hints and large-

• Continuation hints could move incomplete proofs forward; students also found mistakes through unfaithful corrections and sometimes resolved difficult feedback using external resources.Hints were especially useful after valid progress or when a large-jump warning exposed missing intermediate reasoning; difficult feedback could require more time and outside materials.Source: §8.2.3 · p. 12, §8.2.4 · p. 12, §8.2.5 · p. 12

8.3.2 Stuck type 2: Lacking a high-level proof strategy (7 cases).

• Students struggled when accurate feedback exposed low-level obligations or when the system could not distinguish strategically useful steps from merely correct ones.When students lacked a proof strategy, the system could fail on incidental obligations; irrelevant facts outside its mini lemma library could be marked unverified and mislead them.Source: §8.3.1 · pp. 12–13, §8.3.2 · p. 13, §8.3.3 · p. 13

8.4 Participants gained confidence from the verified results

• Verification alone did not immediately raise confidence; students became more confident as they checked that verified claims faithfully represented their intent.Confidence also increased when continuation suggestions or large-jump warnings clarified missing details.Source: §8.4 · p. 13

8.5 Could students obtain extra information from reading Lean code?

• Most students valued knowing code backed the feedback, but reading Lean code usually added little; comments helped three students inspect evidence or confusing results.Those comments provided a detailed logic trace below the granularity of the interface.Source: §8.5 · pp. 13–14

9.2 What could an FVCR system provide?

• LeanSide usually followed students’ reasoning at their granularity, but preserved only the preprocessed smallest progression unit, not lower-level decompositions within it.That unit can be customized to the reasoning task.Source: §9.2 · p. 14
• Verified steps helped students localize faulty logic or gaps by focusing attention on unverified steps, provided the translation was faithful.Students continued until all steps were verified or used their mathematical knowledge to suspect prover failure.Source: §9.2 · p. 14
• Continuation hints and informal Lean-code comments offered students natural-language explanations grounded in verified reasoning.The discussion suggests similar explanations may help in other tasks where users need more than a validity check.Source: §9.2 · p. 14
• Comparing input with less ambiguous informalizations helped students notice ambiguity, clarify assumptions, and make high-level reasoning more rigorous.The discussion frames verification as a mirror for refining strategies into precise reasoning.Source: §9.2 · p. 14

9.3 LeanSide Limitations, and Design Implications for Future FVCR Systems

• Lean’s lower-level proof obligations can make step-level error messages harder to interpret when students state a course-level assertion without further explanation.The discussion suggests counterexample sampling or higher-level LLM feedback as complements, with formal verification potentially checking generated feedback.Source: §9.3 · p. 15
• Lean can flag an incorrect step after several correct ones without identifying where an unproductive proof path diverged strategically.Formal and search-based proofs may not follow the intuitive order in which people understand a proof; strategic hints could complement verification.Source: §9.3 · p. 15
• Task-specific auxiliary components can add useful support around formal verification, with their roles varying by domain and interaction need.The discussion presents this as guidance for designers deciding when to use an FVCR system.Source: §9.3 · p. 15

9.4 Open design challenges: faithfulness checking and auto-detecting contextual granularity

• Faithfulness checks must remain visible without becoming tedious, while delayed interpretation checks let unfaithful earlier steps affect later verification and judgments.Students often checked interpretations only after resolving errors and preparing to submit; an earlier unfaithful step could contribute to later confusion or getting stuck.Source: §9.4 · p. 15

Participant population

• All participants came from one university, and many studied Computer Science, Mathematics, or related fields.Their training may have made them more familiar with formal verification and more inclined to trust its results.Source: §10 · p. 16
• Participants’ disciplinary training may have helped them express informal reasoning more precisely than general users.This could mean their inputs were less ambiguous than those of general users.Source: §10 · p. 16

Problem scope

• The selected problems focused primarily on Linear Algebra and Optimization, so findings may not generalize to other areas of mathematics.The selection reflected the deployment course and the domains where the current modules performed more reliably.Source: §10 · p. 16

Problem set

• Each of the ten EECS 127 problems was attempted by 10 students.Source: A Problem Statements · p. 20

Vector norms

• Vector-norm exercises ask students to prove inequalities relating the infinity, Euclidean, and 1-norms, including dimension-scaled bounds.Source: A Problem Statements · p. 20

Frobenius norm

• Frobenius-norm tasks cover zero characterization, scalar homogeneity, the triangle inequality, and a singular-value expression with a cyclic-trace hint.Source: A Problem Statements · p. 20

Matrix properties

• Other problems ask students to prove that a positive semidefinite matrix has nonnegative diagonal entries and that distinct eigenvalues have orthogonal eigenvectors.Source: A Problem Statements · p. 20

Eigenvalue optimization

• For a symmetric matrix A, students were asked to prove the optimization optimum p*=λ1 by establishing p*≤λ1 and p*≥λ1, with eigenvalues ordered λ0>…>λn−1.Q13 and Q14 were split from Q12 because Q12 took too long to complete in the classroom deployment; the study data for Q12 were retained.Source: A Problem Statements · p. 20

B More interface screenshots

• Figure 14 provides examples of the interface.Source: Figure 14 · p. 21

C Participants’ demographic information

• Table 2 presents participant background and familiarity with Lean.Source: Table 2 · p. 22
• Figure 15 shows students’ grade distribution.Source: Figure 15 · p. 22