Exploring proof autoformalization with Mistral on Herald

DOI10.1007/978-3-032-07021-0_16MaRDI QIDQ6856411zbMATH OpenFDO

Authors Lucy Horowitz, Michail Karatarakis, Xuandi Ren, Alejandro Sanchez Ocegueda

Publication date 19 February 2026

Full work available at URL https://doi.org/10.1007/978-3-032-07021-0_16

zbMATH Keywords

autoformalizationformal mathLean 4LLMmathlib

Mathematics Subject Classification ID

Computer science support for mathematical research and practice (68Vxx)

Cites work

• Automating formalization by statistical and semantic parsing of mathematics
• Developing corpus-based translation methods between informal and formal mathematics: project description
• Duper: a proof-producing superposition theorem prover for dependent type theory
• First experiments with neural translation of informal to formal mathematics
• Proof repair infrastructure for supervised models: building a large proof repair dataset
• The Lean theorem prover (system description)

This page was built for publication: Exploring proof autoformalization with Mistral on Herald

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6856411)