Verified proof, imperfect interpretation
A mathematically verified answer can still misrepresent what a student meant. LeanSide translates students' natural-language proofs into the Lean proof system, checks them, and returns readable feedback. Researchers studied 23 usable sessions alongside an advanced linear-algebra course deployment. Students sometimes repaired errors or made their reasoning more precise, but they also struggled with feedback that was technically correct and difficult to understand. Expert review found that the system changed the meaning of 22 of 117 incorrect steps, compared with 18 of 1,038 correct steps. Some changes silently repaired a student's error. Verification therefore helps only if the translation preserves the reasoning being assessed; a green indicator alone cannot demonstrate student understanding.
Why it matters for leaders
In an AI feedback pilot, show the student's original reasoning beside the system's interpretation. Ask teachers to check whether a tool explains an error or silently solves it. Include incorrect and ambiguous work in acceptance testing, and retain a route to human help when verified feedback is unintelligible.
The evidence
This preprint reports an interface study with expert judgments of reasoning steps and qualitative analysis of student revisions. The course deployment spanned 13 weeks; participants volunteered for study sessions.
Who was studied
University linear algebra; 21 of 23 analyzed participants were undergraduates.
What the evidence cannot tell us
No controlled learning-effect estimate. Advanced university mathematics and prototype behavior do not establish readiness for school mathematics or automated grading.
Read the original sources
Summary and leadership analysis from the Week ending 2026-10-02 brief. The edition’s selection notes explain source access and evidence limitations.