Introduces Relaxed NFL intermediate language for LLM-based auto-formalization, with rule-plus-LLM elaboration to Core NFL and tactic-language discharge of verification conditions.
The role of the Mizar mathematical library for interactive proof development in Mizar
3 Pith papers cite this work. Polarity classification is still indexing.
3
Pith papers citing it
representative citing papers
A multi-agent framework called AutoformBot autoformalized 26 textbooks spanning analysis, algebra, topology, combinatorics and probability into a verified Lean 4 library of 45k declarations, demonstrating scalable formalization of graduate math.
The paper proves Tarski's Axiom A inside Egal and constructs a Grothendieck universe operator inside Mizar, establishing a relationship between the two formalizations of Tarski-Grothendieck set theory.
citing papers explorer
-
Verifiable Auto-Formalization of Mathematics Using a Relaxed Natural Formal Language
Introduces Relaxed NFL intermediate language for LLM-based auto-formalization, with rule-plus-LLM elaboration to Core NFL and tactic-language discharge of verification conditions.
-
Formalizing Mathematics at Scale
A multi-agent framework called AutoformBot autoformalized 26 textbooks spanning analysis, algebra, topology, combinatorics and probability into a verified Lean 4 library of 45k declarations, demonstrating scalable formalization of graduate math.
-
A Tale of Two Set Theories
The paper proves Tarski's Axiom A inside Egal and constructs a Grothendieck universe operator inside Mizar, establishing a relationship between the two formalizations of Tarski-Grothendieck set theory.