% Key papers for Retrieval-augmented formal theorem proving (scime atlas, https://atlas.scime.ai). Authors are not included: add them from the paper pages.

@inproceedings{icml2019_holist_37418,
  title = {{HOList: An Environment for Machine Learning of Higher Order Logic Theorem Proving}},
  booktitle = {International Conference on Machine Learning (ICML)},
  year = {2019},
  url = {https://icml.cc/virtual/2019/poster/3906},
}

@inproceedings{iclr2019_gamepad_29138,
  title = {{GamePad: A Learning Environment for Theorem Proving}},
  booktitle = {International Conference on Learning Representations (ICLR)},
  year = {2019},
  url = {https://iclr.cc/virtual/2019/poster/781},
}

@inproceedings{neurips2023_leandojo_69003,
  title = {{LeanDojo: Theorem Proving with Retrieval-Augmented Language Models}},
  booktitle = {Advances in Neural Information Processing Systems (NeurIPS)},
  year = {2023},
  url = {https://nips.cc/virtual/2023/poster/73510},
}

@inproceedings{iclr2023_draft_32607,
  title = {{Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs}},
  booktitle = {International Conference on Learning Representations (ICLR)},
  year = {2023},
  url = {https://iclr.cc/virtual/2023/poster/11536},
}

@inproceedings{iclr2022_minif2f_30947,
  title = {{miniF2F: a cross-system benchmark for formal Olympiad-level mathematics}},
  booktitle = {International Conference on Learning Representations (ICLR)},
  year = {2022},
  url = {https://iclr.cc/virtual/2022/poster/6258},
}

@inproceedings{iclr2023_formal_31888,
  title = {{Formal Mathematics Statement Curriculum Learning}},
  booktitle = {International Conference on Learning Representations (ICLR)},
  year = {2023},
  url = {https://iclr.cc/virtual/2023/poster/11923},
}

@inproceedings{icml2019_learning_37506,
  title = {{Learning to Prove Theorems via Interacting with Proof Assistants}},
  booktitle = {International Conference on Machine Learning (ICML)},
  year = {2019},
  url = {https://icml.cc/virtual/2019/poster/3658},
}

@inproceedings{neurips2022_thor_65607,
  title = {{Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers}},
  booktitle = {Advances in Neural Information Processing Systems (NeurIPS)},
  year = {2022},
  url = {https://nips.cc/virtual/2022/poster/53223},
}

@inproceedings{neurips2020_learning_60234,
  title = {{Learning to Prove Theorems by Learning to Generate Theorems}},
  booktitle = {Advances in Neural Information Processing Systems (NeurIPS)},
  year = {2020},
  url = {https://nips.cc/virtual/2020/poster/17141},
}

@inproceedings{iclr2024_llemma_33616,
  title = {{Llemma: An Open Language Model for Mathematics}},
  booktitle = {International Conference on Learning Representations (ICLR)},
  year = {2024},
  url = {https://iclr.cc/virtual/2024/poster/19459},
}

@inproceedings{neurips2021_naturalproofs_61908,
  title = {{NaturalProofs: Mathematical Theorem Proving in Natural Language}},
  booktitle = {Advances in Neural Information Processing Systems (NeurIPS)},
  year = {2021},
  url = {https://openreview.net/forum?id=Jvxa8adr3iY},
}

@inproceedings{cvpr2024_e_23299,
  title = {{E-GPS: Explainable Geometry Problem Solving via Top-Down Solver and Bottom-Up Generator}},
  booktitle = {IEEE/CVF Conference on Computer Vision and Pattern Recognition (CVPR)},
  year = {2024},
  url = {https://cvpr.thecvf.com/virtual/2024/poster/30532},
}

@inproceedings{iclr2024_lego_33576,
  title = {{LEGO-Prover: Neural Theorem Proving with Growing Libraries}},
  booktitle = {International Conference on Learning Representations (ICLR)},
  year = {2024},
  url = {https://iclr.cc/virtual/2024/poster/19499},
}

@inproceedings{iclr2024_magnushammer_35259,
  title = {{Magnushammer: A Transformer-Based Approach to Premise Selection}},
  booktitle = {International Conference on Learning Representations (ICLR)},
  year = {2024},
  url = {https://iclr.cc/virtual/2024/poster/17814},
}

@inproceedings{iclr2021_isarstep_30289,
  title = {{IsarStep: a Benchmark for High-level Mathematical Reasoning}},
  booktitle = {International Conference on Learning Representations (ICLR)},
  year = {2021},
  url = {https://iclr.cc/virtual/2021/poster/3049},
}

@inproceedings{neurips2023_satlm_68261,
  title = {{SatLM: Satisfiability-Aided Language Models Using Declarative Prompting}},
  booktitle = {Advances in Neural Information Processing Systems (NeurIPS)},
  year = {2023},
  url = {https://nips.cc/virtual/2023/poster/71537},
}

@inproceedings{neurips2022_naturalprover_66147,
  title = {{NaturalProver: Grounded Mathematical Proof Generation with Language Models}},
  booktitle = {Advances in Neural Information Processing Systems (NeurIPS)},
  year = {2022},
  url = {https://nips.cc/virtual/2022/poster/53914},
}

@inproceedings{iclr2022_proof_31738,
  title = {{Proof Artifact Co-Training for Theorem Proving with Language Models}},
  booktitle = {International Conference on Learning Representations (ICLR)},
  year = {2022},
  url = {https://iclr.cc/virtual/2022/poster/6391},
}

@inproceedings{neurips2024_putnambench_71085,
  title = {{PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition}},
  booktitle = {Advances in Neural Information Processing Systems (NeurIPS)},
  year = {2024},
  url = {https://neurips.cc/virtual/2024/poster/97811},
}

@inproceedings{aaai2024_defeasible_5657,
  title = {{Defeasible Normative Reasoning: A Proof-Theoretic Integration of Logical Argumentation}},
  booktitle = {AAAI Conference on Artificial Intelligence (AAAI)},
  year = {2024},
  url = {https://ojs.aaai.org/index.php/AAAI/article/view/28913},
}

@inproceedings{neurips2024_lean_72479,
  title = {{Lean Workbook: A large-scale Lean problem set formalized from natural language math problems}},
  booktitle = {Advances in Neural Information Processing Systems (NeurIPS)},
  year = {2024},
  url = {https://neurips.cc/virtual/2024/poster/97664},
}

@inproceedings{neurips2024_proving_74550,
  title = {{Proving Theorems Recursively}},
  booktitle = {Advances in Neural Information Processing Systems (NeurIPS)},
  year = {2024},
  url = {https://neurips.cc/virtual/2024/poster/93034},
}

@inproceedings{neurips2025_verithoughts_75029,
  title = {{VeriThoughts: Enabling Automated Verilog Code Generation using Reasoning and Formal Verification}},
  booktitle = {Advances in Neural Information Processing Systems (NeurIPS)},
  year = {2025},
  url = {https://openreview.net/forum?id=3Z8fWHKqlu},
}

@inproceedings{iclr2025_lean_82180,
  title = {{Lean-STaR: Learning to Interleave Thinking and Proving}},
  booktitle = {International Conference on Learning Representations (ICLR)},
  year = {2025},
  url = {https://iclr.cc/virtual/2025/poster/29611},
}

@inproceedings{aaai2024_interactive_6341,
  title = {{Interactive Theorem Provers: Applications in AI, Opportunities, and Challenges}},
  booktitle = {AAAI Conference on Artificial Intelligence (AAAI)},
  year = {2024},
  url = {https://ojs.aaai.org/index.php/AAAI/article/view/30276},
}

@inproceedings{neurips2024_proving_70773,
  title = {{Proving Olympiad Algebraic Inequalities without Human Demonstrations}},
  booktitle = {Advances in Neural Information Processing Systems (NeurIPS)},
  year = {2024},
  url = {https://neurips.cc/virtual/2024/poster/97830},
}

@inproceedings{neurips2025_3d_79544,
  title = {{3D-Prover: Diversity Driven Theorem Proving With Determinantal Point Processes}},
  booktitle = {Advances in Neural Information Processing Systems (NeurIPS)},
  year = {2025},
  url = {https://openreview.net/forum?id=qTUZJUXt0J},
}

@inproceedings{iclr2024_refactor_34896,
  title = {{REFACTOR: Learning to Extract Theorems from Proofs}},
  booktitle = {International Conference on Learning Representations (ICLR)},
  year = {2024},
  url = {https://iclr.cc/virtual/2024/poster/18178},
}

@inproceedings{icml2024_autoformalizing_44838,
  title = {{Autoformalizing Euclidean Geometry}},
  booktitle = {International Conference on Machine Learning (ICML)},
  year = {2024},
  url = {https://icml.cc/virtual/2024/poster/33614},
}

@inproceedings{icml2025_proofaug_46726,
  title = {{ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis}},
  booktitle = {International Conference on Machine Learning (ICML)},
  year = {2025},
  url = {https://icml.cc/virtual/2025/poster/45846},
}

@inproceedings{icml2025_stp_49153,
  title = {{STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving}},
  booktitle = {International Conference on Machine Learning (ICML)},
  year = {2025},
  url = {https://icml.cc/virtual/2025/poster/43472},
}

@inproceedings{icml2026_mathliblemma_49438,
  title = {{MathlibLemma: Folklore Lemma Generation and Benchmark for Formal Mathematics}},
  booktitle = {International Conference on Machine Learning (ICML)},
  year = {2026},
  url = {https://openreview.net/forum?id=2WfRsrQxpC},
}

@inproceedings{icml2026_exverus_50754,
  title = {{ExVerus: Verus Proof Repair via Counterexample Reasoning}},
  booktitle = {International Conference on Machine Learning (ICML)},
  year = {2026},
  url = {https://openreview.net/forum?id=FNDkXA0OUJ},
}

@inproceedings{icml2026_from_51420,
  title = {{From LLM-Generated Conjectures to Lean Formalizations: Automated Polynomial Inequality Proving via Sum-of-Squares Certificates}},
  booktitle = {International Conference on Machine Learning (ICML)},
  year = {2026},
  url = {https://openreview.net/forum?id=Lz8rHDmmKt},
}