FaithSieve uses Lean to improve AI detection of first errors in math proofs
A new preprint introduces FaithSieve, a Lean-assisted framework that breaks AI-generated mathematical proofs into local reasoning units and reports higher first-error localization accuracy than direct model judging.