Bogdan Grechuk

StepProof: Step-by-step verification of natural language mathematical proofs

2025 · arXiv (Cornell University)

Interactive theorem provers (ITPs) are powerful tools for the formal verification of mathematical proofs down to the axiom level. However, their lack of a natural language interface remains a significant limitation. Recent advancements in large …