NLP Wiki

User Tools

Site Tools

Trace:
ml:automatic_theorem_proving

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revisionPrevious revision
Next revision		Previous revision
ml:automatic_theorem_proving [2025/06/02 18:34] – [Neural Theorem Proving] jmflanigml:automatic_theorem_proving [2025/10/07 14:31] (current) – [Autoformalization] jmflanig
Line 7: Line 7:
   * Formalizing mathematics   * Formalizing mathematics
     * [[http://cl-informatik.uibk.ac.at/users/cek/docs/20/ckfr-cicm20.pdf|Kaliszyk & Rabe 2020 - A Survey of Languages for Formalizing Mathematics]]     * [[http://cl-informatik.uibk.ac.at/users/cek/docs/20/ckfr-cicm20.pdf|Kaliszyk & Rabe 2020 - A Survey of Languages for Formalizing Mathematics]]
 +  * Autoformalization
 +    * [[https://arxiv.org/pdf/2505.23486|Weng et al 2025 - Autoformalization in the Era of Large Language Models: A Survey]]
  
 ===== Papers ===== ===== Papers =====
Line 39: Line 41:
     * [[https://arxiv.org/pdf/2303.04910|First et al 2023 - Baldur: Whole-Proof Generation and Repair with Large Language Models]]     * [[https://arxiv.org/pdf/2303.04910|First et al 2023 - Baldur: Whole-Proof Generation and Repair with Large Language Models]]
   * [[https://arxiv.org/pdf/2310.18457|Welleck & Saha 2023 - LLMSTEP: LLM proofstep suggestions in Lean]]   * [[https://arxiv.org/pdf/2310.18457|Welleck & Saha 2023 - LLMSTEP: LLM proofstep suggestions in Lean]]
 +  * [[https://arxiv.org/pdf/2412.20735|Li et al 2024 - HunyuanProver: A Scalable Data Synthesis Framework and Guided Tree Search for Automated Theorem Proving]]
   * [[https://arxiv.org/pdf/2502.00212|Dong & Ma 2025 - STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving]]   * [[https://arxiv.org/pdf/2502.00212|Dong & Ma 2025 - STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving]]
   * [[https://arxiv.org/pdf/2505.20613|Shen et al 2025 - REAL-Prover: Retrieval Augmented Lean Prover for Mathematical Reasoning]]   * [[https://arxiv.org/pdf/2505.20613|Shen et al 2025 - REAL-Prover: Retrieval Augmented Lean Prover for Mathematical Reasoning]]
Line 80: Line 83:
 ===== Autoformalization ===== ===== Autoformalization =====
   * Overviews   * Overviews
 +    * [[https://leanprover.zulipchat.com/user_uploads/3121/lWKHE1MCcJ1ZwiF2poPoJckC/Autoformalization.pdf|Szegedy 2019 - A Promising Path Towards Autoformalization and General Artificial Intelligence]] Great
     * [[https://arxiv.org/pdf/2311.00007|Avigad et al 2023 - Mathematics and the Formal Turn]] Great overview of the reasons to autoformalize mathematics     * [[https://arxiv.org/pdf/2311.00007|Avigad et al 2023 - Mathematics and the Formal Turn]] Great overview of the reasons to autoformalize mathematics
 +    * [[https://arxiv.org/pdf/2505.23486|Weng et al 2025 - Autoformalization in the Era of Large Language Models: A Survey]]
  
 === Informal Math to Formal Math Parsing === === Informal Math to Formal Math Parsing ===
ml/automatic_theorem_proving.1748889294.txt.gz · Last modified: 2025/06/02 18:34 by jmflanig
Donate Powered by PHP Valid HTML5 Valid CSS Driven by DokuWiki