mlsanityData to 7 Oct 2026

First Experiments with Neural Translation of Informal to Formal Mathematics

arXiv 1805.06502 ↗First posted 10 May 2018cs.CL cs.AI cs.LGcited by 52

Not on the map. Why?

Abstract (arXiv)

We report on our experiments to train deep neural networks that automatically translate informalized LaTeX-written Mizar texts into the formal Mizar language. To the best of our knowledge, this is the first time when neural networks have been adopted in the formalization of mathematics. Using Luong et al.'s neural machine translation model (NMT), we tested our aligned informal-formal corpora against various hyperparameters and evaluated their results. Our experiments show that our best performing model configurations are able to generate correct Mizar statements on 65.73% of the inference data, with the union of all models covering 79.17%. These results indicate that formalization through artificial neural network is a promising approach for automated formalization of mathematics. We present several case studies to illustrate our results.

Key facts. Cited by 52 papers in the map (data through 7 Oct 2026). First posted on arXiv 10 May 2018.

Builds on

No reference list yet.

Built on by

Cited by year (2026 to 7 Oct)

Citing papers per year: 2021: 3; 2022: 3; 2023: 11; 2024: 10; 2025: 19; 2026: 6.

52 papers.

Sort:

By area:

  1. 2023A Survey of Large Language Modelscited by 2,537
  2. 2023LeanDojo: Theorem Proving with Retrieval-Augmented Language Modelscited by 414
  3. 2022Autoformalization with Large Language Modelscited by 252
  4. 2023ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematicscited by 180
  5. 2023LINC: A Neurosymbolic Approach for Logical Reasoning by Combining Language Models with First-Order Logic Proverscited by 161
  6. 2021Proof Artifact Co-training for Theorem Proving with Language Modelscited by 130
  7. 2023LEGO-Prover: Neural Theorem Proving with Growing Librariescited by 108
  8. 2024Formal Mathematical Reasoning: A New Frontier in AIcited by 80
  9. 2024A Survey on Deep Learning for Theorem Provingcited by 55
  10. 2024Herald: A Natural Language Annotated Lean 4 Datasetcited by 54
  11. 2024Process-Driven Autoformalization in Lean 4cited by 45
  12. 2023Multilingual Mathematical Autoformalizationcited by 38
38 more
  1. 2022Formal Specifications from Natural Languagecited by 33
  2. 2023Towards Autoformalization of Mathematics and Code Correctness: Experiments with Elementary Proofscited by 27
  3. 2024Autoformalizing Euclidean Geometrycited by 27
  4. 2025ATLAS: Autoformalizing Theorems through Lifting, Augmentation, and Synthesis of Datacited by 23
  5. 2022Towards a Mathematics Formalisation Assistant using Large Language Modelscited by 22
  6. 2024FormalAlign: Automated Alignment Evaluation for Autoformalizationcited by 19
  7. 2025Aria: An Agent For Retrieval and Iterative Auto-Formalization via Dependency Graphcited by 18
  8. 2026130k Lines of Formal Topology in Two Weeks: Simple and Cheap Autoformalization for Everyone?cited by 16
  9. 2025miniF2F-Lean Revisited: Reviewing Limitations and Charting a Path Forwardcited by 13
  10. 2023Alien Codingcited by 9
  11. 2024GFLean: An Autoformalisation Framework for Lean via GFcited by 9
  12. 2025Grammars of Formal Uncertainty: When to Trust LLMs in Automated Reasoning Taskscited by 9
  13. 2025Generalized Tree Edit Distance (GTED): A Faithful Evaluation Metric for Statement Autoformalizationcited by 9
  14. 2025ASSESS: A Semantic and Structural Evaluation Framework for Statement Similaritycited by 8
  15. 2025A Neurosymbolic Approach to Natural Language Formalization and Verificationcited by 8
  16. 2023Neural Machine Translation for Mathematical Formulaecited by 7
  17. 2024Learning Guided Automated Reasoning: A Brief Surveycited by 7
  18. 2024FLARE: Faithful Logic-Aided Reasoning and Explorationcited by 7
  19. 2025Towards a Common Framework for Autoformalizationcited by 7
  20. 2025Lean Finder: Semantic Search for Mathlib That Understands User Intentscited by 7
  21. 2023MizAR 60 for Mizar 50cited by 6
  22. 20243D-Prover: Diversity Driven Theorem Proving With Determinantal Point Processescited by 6
  23. 2025HybridProver: Augmenting Theorem Proving with LLM-Driven Proof Synthesis and Refinementcited by 6
  24. 2021A Study of Continuous Vector Representationsfor Theorem Provingcited by 4
  25. 2025Lean-ing on Quality: How High-Quality Data Beats Diverse Multilingual Data in AutoFormalizationcited by 4
  26. 2025Thinking Machines: Mathematical Reasoning in the Age of LLMscited by 4
  27. 2025Learning Conjecturing from Scratchcited by 3
  28. 2025A Llama walks into the 'Bar': Efficient Supervised Fine-Tuning for Legal Reasoning in the Multi-state Bar Examcited by 3
  29. 2026The Faithfulness Gap: Certifying Semantic Equivalence Between Natural-Language and Formal Mathematical Statementscited by 3
  30. 2025Improving Autoformalization Using Direct Dependency Retrievalcited by 2
  31. 2021Disambiguating Symbolic Expressions in Informal Documentscited by 1
  32. 2025Hierarchical Attention Generates Better Proofscited by 1
  33. 2025Towards Generating Controllable and Solvable Geometry Problem by Leveraging Symbolic Deduction Enginecited by 1
  34. 2025KELPS: A Framework for Verified Multi-Language Autoformalization via Semantic-Syntactic Alignmentcited by 1
  35. 2026Munkres' General Topology Autoformalized in Isabelle/HOLcited by 1
  36. 2026Decompose, Structure, and Repair: A Neuro-Symbolic Framework for Autoformalization via Operator Treescited by 1
  37. 2023Translating SUMO-K to Higher-Order Set Theorycited by 0
  38. 2025TopoAlign: A Framework for Aligning Code to Math via Topological Decompositioncited by 0

50 most cited of 52 All 52 (JSON)