Bibliography

Every work this repository cites, once: Key, citation, and a stable link.

Shape: references

Key	Citation	Link
Adamczewski 2026	Adamczewski (2026). fc-review-results: an automated audit of formal-conjectures; README and the metadata of run c90271f0fa, 2026-09-11. GitHub repository	https://github.com/tadamcz/fc-review-results
Adams 2016	Adams (2016). Proof auditing formalised mathematics. Journal of Formalized Reasoning 9(1), special issue Twenty years of the QED manifesto	https://doi.org/10.6092/issn.1972-5787/4576
Aitken 1998	Aitken, Gray, Melham, Thomas (1998). Interactive theorem proving: an empirical study of user activity. Journal of Symbolic Computation 25(2). Read through Ringer 2019	https://doi.org/10.1006/jsco.1997.0175
Aitken 2000	Aitken, Melham (2000). An analysis of errors in interactive proof attempts. Interacting with Computers 12(6), 565-586. Read in full through the university	https://doi.org/10.1016/S0953-5438(99)00023-5
Alexeev 2025	Alexeev (2025-12-05). Formalization of Erdős problems. Guest post, Xena Project blog	https://xenaproject.wordpress.com/2025/12/05/formalization-of-erdos-problems/
Ammanamanchi 2026	Ammanamanchi, Bhat, Biderman (2026). Faults in our formal benchmarking: dataset defects and evaluation failures in Lean theorem proving. ICML 2026	arXiv:2606.29493
Anthropic 2026c	Anthropic (2026). Fermat's Last Theorem. Research page; the owner's account of its own work	https://www.anthropic.com/research/formalizing-fermats-last-theorem (archived: https://web.archive.org/web/20261023034152/https://www.anthropic.com/research/formalizing-fermats-last-theorem)
Avigad 2019	Avigad (2019). Learning logic and proof with an interactive theorem prover. In Hanna, Reid, de Villiers (eds.), Proof Technology in Mathematics Research and Teaching, Springer, 277-290	https://doi.org/10.1007/978-3-030-28483-1_13
Avigad 2024	Avigad (2024). Mathematics and the formal turn. Bulletin of the AMS 61(2), 225-240; preprint arXiv 2311.00007	https://doi.org/10.1090/bull/1832
Avigad 2026	Avigad, Buzzard, Commelin, Degenne, Morrison, Nash, Topaz (2026-10-16). How to formalize all of mathematics. Guest post, Xena Project blog	https://xenaproject.wordpress.com/2026/10/16/how-to-formalize-all-of-mathematics/
Axiom 2026	Axiom (2026-01-08). From seeing why to checking everything. Research page; the owner's account	https://axiommath.ai/research/from-seeing-why-to-checking-everything (archived: https://web.archive.org/web/20261012022104/https://axiommath.ai/research/from-seeing-why-to-checking-everything/)
Azerbayev 2023	Azerbayev, Piotrowski, Schoelkopf, Ayers, et al. (2023). ProofNet: autoformalizing and formally proving undergraduate-level mathematics. Preprint	arXiv:2302.12433
Bancerek 2017	Bancerek, Byliński, Grabowski, Korniłowicz, Matuszewski, Naumowicz, Pąk (2017). The role of the Mizar Mathematical Library for interactive proof development in Mizar. Journal of Automated Reasoning 61, 9-32 (online November 2017; volume 61 is the 2018 print volume)	https://doi.org/10.1007/s10817-017-9440-6
Barendregt 2005	Barendregt, Wiedijk (2005). The challenge of computer mathematics. Philosophical Transactions of the Royal Society A 363, 2351-2375	https://doi.org/10.1098/rsta.2005.1650
Barik 2017	Barik, Smith, Lubick, Holmes, Feng, Murphy-Hill, Parnin (2017). Do developers read compiler error messages? ICSE 2017, 575-585. Abstract read	https://doi.org/10.1109/ICSE.2017.59
Bartzia 2026	Bartzia, Beffara, Meyer, Narboux (2026). Proof assistants for undergraduate mathematics education: elements of an a priori analysis. International Journal of Mathematical Education in Science and Technology, 1-44	https://doi.org/10.1080/0020739x.2026.2632264
Bastani 2025	Bastani, Bastani, Sungu, Ge, Kabakcı, Mariman (2025). Generative AI without guardrails can harm learning: evidence from high school mathematics. Proceedings of the National Academy of Sciences 122(26), e2422633122. Abstract read (Crossref)	https://doi.org/10.1073/pnas.2422633122
Bastounis 2026	Bastounis, Circelli, Hansen (2026). Navier-Stokes lost in translation: why Lean verification of AI autoformalisation does not guarantee correct natural language proofs. Preprint	arXiv:2610.08144
Becker 2016	Becker (2016). An effective approach to enhancing compiler error messages. SIGCSE 2016, 126-131. Abstract read; the open copy refused automated reads	https://doi.org/10.1145/2839509.2844584
Becker 2019	Becker, Denny, Pettit, Bouchard, Bouvier, Harrington and others (2019). Compiler error messages considered unhelpful: the landscape of text-based programming error message research. ITiCSE Working Group Reports, 177-210. Read in full through the university	https://doi.org/10.1145/3344429.3372508
Becker 2024	Becker, de Frutos-Fernández, Diedering, van Doorn, Gouëzel and others (2024). A blueprint for the formalization of Carleson's theorem on convergence of Fourier series. Preprint	arXiv:2405.06423
Beckert 2014	Beckert, Grebing, Böhl (2014). How to put usability into focus: using focus groups to evaluate the usability of interactive theorem provers. UITP 2014, EPTCS 167, 4-13	https://doi.org/10.4204/EPTCS.167.3
Beckert 2015	Beckert, Grebing, Böhl (2015). A usability evaluation of interactive theorem provers using focus groups. Software Engineering and Formal Methods workshops, LNCS, 3-19. Not read; its finding is cited through Ringer 2019	https://doi.org/10.1007/978-3-319-15201-1_1
Binder 2026	Binder, Lachnitt, Kosaian (2026). Apply2Isar: automatically converting Isabelle/HOL apply-style proofs to structured Isar. Preprint	arXiv:2603.07771
Blanchette 2016	Blanchette, Kaliszyk, Paulson, Urban (2016). Hammering towards QED. Journal of Formalized Reasoning 9(1). DOI not on Crossref; resolved through doi.org	https://doi.org/10.6092/issn.1972-5787/4593
Böhne 2018	Böhne, Kreitz (2018). Learning how to prove: from the Coq proof assistant to textbook style. EPTCS 267, 1-18	https://doi.org/10.4204/eptcs.267.1
Bolan 2025	Bolan, Breitner, Brox, Carlini, Carneiro and others, with Tao (2025). The Equational Theories Project: advancing collaborative mathematical research at scale. Preprint	arXiv:2512.07087
Bottoni 2025	Bottoni, Cattaneo, Saçıkara (2025). Teaching "Foundations of Mathematics" with the Lean theorem prover. Preprint	arXiv:2501.03352
Browning 2026	Browning, Hristova, Ledvinka, Springer, et al. (2026). A dataset of formalised theorem statements from the Annals of Mathematics. AI-MATH workshop, NeurIPS 2026	arXiv:2610.18301
Buçinca 2021	Buçinca, Malaya, Gajos (2021). To trust or to think: cognitive forcing functions can reduce overreliance on AI in AI-assisted decision-making. Proceedings of the ACM on Human-Computer Interaction 5(CSCW1), 1-21	https://doi.org/10.1145/3449287
Buzzard 2024	Buzzard (2024-12-11). Fermat's Last Theorem: how it's going. Xena Project blog	https://xenaproject.wordpress.com/2024/12/11/fermats-last-theorem-how-its-going/
Buzzard 2025	Buzzard (2025-10-22). Formal or not formal? That is the question in AI for theorem proving. Xena Project blog	https://xenaproject.wordpress.com/2025/10/22/formal-or-not-formal-that-is-the-question-in-ai-for-theorem-proving/
Buzzard 2026a	Buzzard (2026-09-04). FLT: Anthropic has beaten me to it. Xena Project blog; read by both sides, and again by the maintainer's session	https://xenaproject.wordpress.com/2026/09/04/flt-anthropic-has-beaten-me-to-it/
Buzzard 2026b	Buzzard (2026-08-13). The Annals Challenge. Xena Project blog	https://xenaproject.wordpress.com/2026/08/13/the-annals-challenge/
Buzzard 2026c	Buzzard (2026-10-01). To grieve, or not to grieve? Xena Project blog	https://xenaproject.wordpress.com/2026/10/01/to-grieve-or-not-to-grieve/
Buzzard 2026d	Buzzard (2026-07-20). Human mathematicians are being outcounterexampled. Xena Project blog	https://xenaproject.wordpress.com/2026/07/20/human-mathematicians-are-being-outcounterexampled/
Carl 2020	Carl (2020). Using automated theorem provers for mistake diagnosis in the didactics of mathematics. Preprint	arXiv:2002.05083
Carl 2020b	Carl (2020). Automatized evaluation of formalization exercises in mathematics. Preprint	arXiv:2006.01800
Carl 2022	Carl, Lorenzen, Schmitz (2022). Natural language proof checking in introduction to proof classes: first experiences with Diproche. ThEdu'21, EPTCS 354, 59-70	https://doi.org/10.4204/EPTCS.354.5
Carl 2024	Carl (2024). Improving the Diproche CNL through autoformalization via large language models. ThEdu'23, EPTCS 400, 44-58	https://doi.org/10.4204/EPTCS.400.4
Carneiro 2024	Carneiro (2024). Lean4Lean: verifying a typechecker for Lean, in Lean. Preprint	arXiv:2403.14064
Carter 2013	Carter, Monks (2013). Lurch: a word processor that can grade students' proofs. CICM 2013 Workshops and Work in Progress, CEUR-WS 1010, paper 4	https://ceur-ws.org/Vol-1010/paper-04.pdf
Chen 2025	Chen, Wu, Chen, et al. (2025). ReForm: reflective autoformalization with prospective bounded sequence optimization. ICLR 2026	arXiv:2510.24592
Chen 2026b	Chen, Marwaha, Lu, Yuen, Peng (2026). Prove2Me: an open collaborative platform for scaling math formalization. Preprint	arXiv:2608.28433
Chung 2026	Chung, Cai, Li, Yin, Agarwal and others, with Arora (2026). Goedel-Architect: streamlining formal theorem proving with blueprint generation and refinement. Preprint	arXiv:2606.06468
CMU L3 2025	cmu-l3 (2025, news to October 2025, read 2026). LLMLean: LLMs and Lean for tactic suggestions and proof completion. GitHub repository README	https://github.com/cmu-l3/llmlean
Collins 2024	Collins, Jiang, Frieder, Wong, Zilka, Bhatt, Lukasiewicz, Wu, Tenenbaum, Hart, Gowers, Li, Weller, Jamnik (2024). Evaluating language models for mathematics through interactions. PNAS 121(24); preprint arXiv 2306.01694	https://doi.org/10.1073/pnas.2318124121
Collins 2026	Collins, Frieder, Bayer, Loader, Lim, Song, Zaiser, Zhou, Li, Looi, Tenenbaum, Bhatt, Weller, Hernandez-Orallo, Freer, Chen, Sucholutsky (2026). Human agency in initial human-AI proof formalization workflows. Preprint	arXiv:2606.04273
Commelin 2024	Commelin, Topaz (2024). Abstraction boundaries and spec driven development in pure mathematics. Bulletin of the AMS 61, 241-255. Read in the preprint	https://doi.org/10.1090/bull/1831 (arXiv:2309.14870)
Commelin 2026	Commelin, Jamnik, Ochigame, Taelman, Venkatesh (2026). Shaping the future of mathematics in the age of AI. Preprint	arXiv:2603.24914
Corbineau 2008	Corbineau (2008). A declarative language for the Coq proof assistant. TYPES 2007, LNCS 4941, 69-84. Title and venue only	https://doi.org/10.1007/978-3-540-68103-8_5
Coscoy 1995	Coscoy, Kahn, Théry (1995). Extracting text from proofs. TLCA 1995, LNCS 902, 109-123. Title and venue only	https://doi.org/10.1007/BFb0014048
Cramer 2010	Cramer, Fisseni, Koepke, Kühlwein, Schröder, Veldman (2010). The Naproche project: controlled natural language proof checking of mathematical texts. CNL 2009, LNCS 5972, 170-186. Title and venue only	https://doi.org/10.1007/978-3-642-14418-9_11
Cramer 2013	Cramer (2013). Proof-checking mathematical texts in controlled natural language. Doctoral dissertation, Universität Bonn	https://hdl.handle.net/20.500.11811/5780
Dai 2026	Dai, Yan, Lin (2026). The signal-coverage matrix: stratifying type and semantic errors in statement autoformalization. Preprint	arXiv:2606.28013
DeepSeek 2025	DeepSeek (2025-04-30). DeepSeek-Prover-V2-671B. Model card; the owner's results	https://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-671B
De Lon 2021	De Lon, Koepke, Lorenzen, Marti, Schütz, Wenzel (2021). The Isabelle/Naproche natural language proof assistant. CADE-28, LNCS 12699, 614-624	https://doi.org/10.1007/978-3-030-79876-5_36
Deng 2026	Deng, Farber, Narasimha, Sivakumar, Xue (2026). Fix, not just resample: bounded compiler-guided repair in Lean 4. Preprint	arXiv:2610.26942
Denny 2014	Denny, Luxton-Reilly, Carpenter (2014). Enhancing syntax error messages appears ineffectual. ITiCSE 2014, 273-278. Abstract read	https://doi.org/10.1145/2591708.2591748
Denny 2020	Denny, Prather, Becker (2020). Error message readability and novice debugging performance. ITiCSE 2020, 480-486. Abstract read	https://doi.org/10.1145/3341525.3387384
Denny 2021	Denny, Prather, Becker, Mooney, Homer, Albrecht, Powell (2021). On designing programming error messages for novices: readability and its constituent factors. CHI 2021. Abstract read	https://doi.org/10.1145/3411764.3445696
De Toffoli 2024	De Toffoli (2024). Proofs for a price: tomorrow's ultra-rigorous mathematical culture. Bulletin of the AMS 61	https://doi.org/10.1090/bull/1823
Dressler 2026	Dressler (undated, read 2026). lean-lsp-mcp: Lean theorem prover MCP. GitHub repository README	https://github.com/oOo0oOo/lean-lsp-mcp
Erdős DB 2026	Tao and contributors (read 2026). erdosproblems database: README and summary statistics, generated 2026-10. GitHub repository	https://github.com/teorth/erdosproblems/blob/main/STATISTICS.md
Erdős-wiki 2026	erdosproblems contributors (2026). AI contributions to Erdős problems. Wiki page, data as of 2026-06-30 (may move)	https://github.com/teorth/erdosproblems/wiki/AI-contributions-to-Erd%C5%91s-problems
Eremondi 2019	Eremondi, Swierstra, Hage (2019). A framework for improving error messages in dependently-typed languages. Open Computer Science 9(1), 1-32	https://doi.org/10.1515/comp-2019-0001
Fan 2025	Fan, Tang, Le, Shen, Tan, Zhao, Shen, Li, Gašević (2025). Beware of metacognitive laziness: effects of generative artificial intelligence on learning motivation, processes, and performance. British Journal of Educational Technology 56, 489-530	https://doi.org/10.1111/bjet.13544
Feng 2026	Feng, Mao, Arekar, Zhong, Huang, Si, Li (2026). Aligning faithfulness for theory-scale autoformalization: FaithAlign. Preprint	arXiv:2610.18498
Firsching 2026	Firsching, Lezeau, Mercuri, Horváth, et al. (2026). Formal Conjectures: an open and evolving benchmark for verified discovery in mathematics. Preprint	arXiv:2605.13171
First 2023	First, Rabe, Ringer, Brun (2023). Baldur: whole-proof generation and repair with large language models. ESEC/FSE 2023	https://doi.org/10.1145/3611643.3616243 (arXiv:2303.04910)
Fuller 2014	Fuller, Weber, Mejía-Ramos, Rhoads, Samkoff (2014). Comprehending structured proofs. JIEEM 7(1).	https://openalex.org/W2184046398
Gadgil 2026	Gadgil (undated, read 2026). LeanAide: AI-based tools for the Lean theorem prover. GitHub repository README	https://github.com/siddhartha-gadgil/LeanAide
Ganesalingam 2017	Ganesalingam, Gowers (2017). A fully automatic theorem prover with human-style output. Journal of Automated Reasoning 58(2), 253-291 (online 2016). Read in the preprint, whose earlier title says problem solver for theorem prover	https://doi.org/10.1007/s10817-016-9377-1 (arXiv:1309.4501)
Gao 2025	Gao, Wang, Jiang, et al. (2025). Herald: a natural language annotated Lean 4 dataset. ICLR 2025	arXiv:2410.10878
Garousi 2019	Garousi, Felderer, Mäntylä (2019). Guidelines for including grey literature and conducting multivocal literature reviews in software engineering. Information and Software Technology 106, 101-121	https://doi.org/10.1016/j.infsof.2018.09.006
GasStationManager 2026	GasStationManager (undated, read 2026). LeanTool: helping LLMs be better at Lean. GitHub repository README	https://github.com/GasStationManager/LeanTool
GitHub 2026e	GitHub (read 2026-10-29). Public metadata (stars, last push) of the repositories named in review.md, through the unauthenticated API: 23 repositories and one repository search by the formal side, and LeanDojo by the human side. The reviewers' count	https://api.github.com/repos/PatrickMassot/leanblueprint (one of the calls)
GitHub 2026f	GitHub (read 2026-10-29). Formal Conjectures issues and pull requests by the labels misformalization and ai-audit, and their states, through GitHub search. The human side's count, checked again at the audit the same day	https://github.com/google-deepmind/formal-conjectures/issues?q=label%3Amisformalization
GitHub 2026g	GitHub (read 2026-10-29). PNT+ pull requests with and without the ai label, by state, through GitHub search. The human side's count	https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/pulls?q=label%3Aai
GitHub 2026i	GitHub (read 2026-10-29). PNT+ repository at commit 127b50e (2026-10-20): the workflow files under .github/workflows and lakefile.toml, through the unauthenticated public API; no comparator step, challenge file or formalization.yaml in the tree. The reviewer's read	https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/tree/127b50e33f6033e2147921167a117af96d9ba4ea/.github/workflows
Gleirscher 2023	Gleirscher, Sachtleben, Peleska (2023). Qualification of proof assistants, checkers, and generators: where are we and what next? Science of Computer Programming, article 102930; preprint arXiv 2302.09546	https://doi.org/10.1016/j.scico.2023.102930
Gloeckle 2026	Gloeckle, Rammal, Arnal, Munos, Cabannes, Synnaeve, Hayat (2026). Automatic textbook formalization. Preprint; the owners' account	arXiv:2604.03071
Goddard 2012	Goddard, Roudsari, Wyatt (2012). Automation bias: a systematic review of frequency, effect mediators, and mitigators. Journal of the American Medical Informatics Association 19(1), 121-127	https://doi.org/10.1136/amiajnl-2011-000089
Goedel-LM 2025	Goedel-LM (2025-07-14). Goedel-Prover-V2-32B. Model card; the owner's results	https://huggingface.co/Goedel-LM/Goedel-Prover-V2-32B
Gonthier 2013	Gonthier, Asperti, Avigad, Bertot, Cohen, Garillot, Le Roux, Mahboubi, and others (2013). A machine-checked proof of the odd order theorem. ITP 2013, LNCS 7998, 163-179	https://doi.org/10.1007/978-3-642-39634-2_14
Google 2025	Cohen-Addad, Woodruff (2025, updated 2026-05-18). Gemini-backed Paper Assistant Tool provides automated feedback for theoretical computer scientists at STOC 2026. Google Research blog; the owner's account of its own tool (may move)	https://research.google/blog/gemini-provides-automated-feedback-for-theoretical-computer-scientists-at-stoc-2026/
Google DeepMind 2026	Google DeepMind and the Formal Conjectures authors (undated, read 2026). formal-conjectures: README and contributing guide. GitHub repository; read by both sides	https://github.com/google-deepmind/formal-conjectures
Gopinathan 2023	Gopinathan, Keoliya, Sergey (2023). Mostly automated proof repair for verified libraries. PACMPL 7(PLDI), 25-49	https://doi.org/10.1145/3591221
Grabowski 2010	Grabowski, Korniłowicz, Naumowicz (2010). Mizar in a nutshell. Journal of Formalized Reasoning 3(2). DOI not on Crossref; resolved through doi.org	https://doi.org/10.6092/issn.1972-5787/1980
Gui 2026	Gui, Yang, Shi (2026). Evaluating the robustness of proof autoformalization in Lean 4. Preprint	arXiv:2606.14867
Guo 2026b	Guo, Patel, Mehta, Kothari, Lu, Voss, Bhattacharyya, Donovan, Hartmann, Ranade (2026). LeanSide: a formally verified co-reasoning system for natural-language proofs. Preprint	arXiv:2610.00760
Hales 2017	Hales, Adams, Bauer, Dang, Harrison, Hoang, Kaliszyk, Magron, and others (2017). A formal proof of the Kepler conjecture. Forum of Mathematics, Pi 5, e2	https://doi.org/10.1017/fmp.2017.1
Hales 2026	Hales (2026-10-09). What mathematicians should know about the Lean theorem prover: questions of reliability and AI. Guest post on Tao's blog; read by both sides, and again at the merge	https://terrytao.wordpress.com/2026/10/09/what-mathematicians-should-know-about-the-lean-theorem-proverquestions-of-reliability-and-ai/
Han 2026	Han, Kim, Park, et al. (2026). SHADOWBENCH: toward reliable automatic evaluation of semantic alignment in autoformalization. EMNLP 2026	arXiv:2608.29270
Hanna 2021	Hanna, Yan (2021). Opening a discussion on teaching proof with automated theorem provers. For the Learning of Mathematics 41(3), 42-46. Paywalled; read through Tran Minh 2025	https://www.jstor.org/stable/27091220
Hanna 2024	Hanna, Larvor, Yan (2024). Using the proof assistant Lean in undergraduate mathematics classrooms. ZDM Mathematics Education 56, 1517-1529. Read in the authors' copy	https://doi.org/10.1007/s11858-024-01577-9
Harmonic 2024	Harmonic (2024-07-09). One month in: a new SOTA on MiniF2F and more. Company news page; the owner's results	https://harmonic.fun/news/minif2f/ (archived: https://web.archive.org/web/20260521005251/https://www.harmonic.fun/news/minif2f/)
Harrison 1998	Harrison (1998). Proof style. TYPES 1996, LNCS 1512, 154-172	https://doi.org/10.1007/BFb0097791
Harrison 2006	Harrison (2006). Towards self-verification of HOL Light. IJCAR 2006, LNCS 4130, 177-191. Paywalled	https://doi.org/10.1007/11814771_17
Hattori 2025	Hattori, Matsuzaki, Fujiwara (2025). Natural language translation of formal proofs through informalization of proof steps and recursive summarization along proof structure. INLG 2025	arXiv:2509.09726
Hentschel 2016	Hentschel, Hähnle, Bubel (2016). An empirical evaluation of two user interfaces of an interactive program verifier. ASE 2016, 403-413. Read in full through the university	https://doi.org/10.1145/2970276.2970303
Hu 2025	Hu, Zhou, Grechuk, Tyukin (2025). StepProof: step-by-step verification of natural language mathematical proofs. Preprint	arXiv:2506.10558
Hubert 2025	Hubert, Mehta, Sartran, Horváth, Žužić, Wieser, et al. (2025). Olympiad-level formal mathematical reasoning with reinforcement learning. Nature, 607-613	https://doi.org/10.1038/s41586-025-09833-y
Iannone 2023	Iannone, Thoma (2023). Interactive theorem provers for university mathematics: an exploratory study of students' perceptions. International Journal of Mathematical Education in Science and Technology 55, 2622-2644	https://doi.org/10.1080/0020739x.2023.2178981
Iannone 2025a	Iannone, Marasingha, Thoma (2025). Teaching mathematics with Lean: interactive theorem provers in the classroom. Notices of the AMS 72. Not reached: the publisher's page asked for a browser check	https://doi.org/10.1090/noti3184
Iannone 2025b	Iannone, Thoma (2025). "It feels like sort of cheating ...": mathematics students coding proofs with an interactive theorem prover. Digital Experiences in Mathematics Education 12, 366-392	https://doi.org/10.1007/s40751-025-00193-w
Ilin 2026	Ilin, Nugent (2026). Sorries are not the hard part: an expert-review case study of a semi-autonomous formalization. Preprint	arXiv:2606.13925
Isabelle 2026	Isabelle developers (undated, read 2026). Overview. Isabelle website	https://isabelle.in.tum.de/overview.html
Ishii 2014	Ishii, Asai (2014). Report on a user test and extension of a type debugger for novice programmers. TFPIE 2014, EPTCS 170, 1-18	https://doi.org/10.4204/EPTCS.170.1
Jiang 2023c	Jiang, Welleck, Zhou, Li, Liu, Jamnik, Lacroix, Wu, Lample (2023). Draft, sketch, and prove: guiding formal theorem provers with informal proofs. ICLR 2023	arXiv:2210.12283
Kalyuga 2003	Kalyuga, Ayres, Chandler, Sweller (2003). The expertise reversal effect. Educational Psychologist	https://doi.org/10.1207/S15326985EP3801_4
Kamoi 2024	Kamoi, Zhang, Zhang, Han, Zhang (2024). When Can LLMs Actually Correct Their Own Mistakes? A Critical Survey of Self-Correction of LLMs. Transactions of the ACL 12.	doi:10.1162/tacl_a_00713
Kerjean 2022	Kerjean, Le Roux, Massot, Mayero, Mesnil, Modeste, Narboux, Rousselin (2022). Utilisation des assistants de preuves pour l'enseignement en L1. La Gazette de la Société Mathématique de France 174, 35-55. Read through Ouvrier-Buffet 2026	https://hal.science/hal-03979238
Kim 2026b	Kim, Poiroux, Bosselut (2026). Do LLMs game formalization? Evaluating faithfulness in logical reasoning. VerifAI-2 workshop, ICLR 2026, non-archival	arXiv:2604.19459
Kirov 2026a	Kirov (2026-02-08). Leaning on AI. Blog	https://rkirov.github.io/posts/lean5/
Kirov 2026b	Kirov (2026-03-08). Human intuition, AI formalization: a real analysis case study. Blog	https://rkirov.github.io/posts/lean6/
Klowden 2026	Klowden, Tao (2026). Mathematical methods and human thought in the age of AI. Preprint	arXiv:2603.26524
Knobelsdorf 2017	Knobelsdorf, Frede, Böhne, Kreitz (2017). Theorem provers as a learning tool in theory of computation. ICER 2017, 83-92	https://doi.org/10.1145/3105726.3106184
Kondylidou 2026	Kondylidou, Blanchette, Heule (2026). Tao's equational proof challenge accepted. IJCAR 2026, LNCS, 3-21; read in the technical report, arXiv 2605.21200	https://doi.org/10.1007/978-3-032-32589-1_1
Kosmyna 2025	Kosmyna, Hauptmann, Yuan, Situ, Liao, Beresnitzky, Braunstein, Maes (2025). Your brain on ChatGPT: accumulation of cognitive debt when using an AI assistant for essay writing task. Preprint	arXiv:2506.08872
Koutsoukou-Argyraki 2020	Koutsoukou-Argyraki (2020). Formalising mathematics in praxis: a mathematician's first experiences with Isabelle/HOL and the why and how of getting started. Jahresbericht der Deutschen Mathematiker-Vereinigung 123, 3-26 (online 2020, print 2021)	https://doi.org/10.1365/s13291-020-00221-1
Krishnamurthi 2026	Krishnamurthi, Flatt (2026). Type-error ablation and AI coding agents. Preprint	arXiv:2606.01522
Kuhn 2014	Kuhn (2014). A survey and classification of controlled natural languages. Computational Linguistics 40(1), 121-170	https://doi.org/10.1162/COLI_a_00168
Kung 2026	Kung, Song, Hwang, Yoon, Li, Severini, Olšák, Lockhart, Le, Gokturk, Luong, Pfister, Peng (2026). LEAP: supercharging LLMs for formal mathematics with agentic frameworks. Preprint	arXiv:2606.03303
Lean-community 2026	Lean community (undated, read 2026). lean4game documentation, file create_game.md, section on hints	https://github.com/leanprover-community/lean4game/blob/main/doc/create_game.md
LeanDojo 2026	lean-dojo (undated, read 2026). Lean Copilot: LLMs as copilots for theorem proving in Lean. GitHub repository README	https://github.com/lean-dojo/LeanCopilot
Lean FRO 2025	Lean FRO (2025-08-14). Lean 4.22.0 release notes, section Named errors with explanations. The Lean language reference	https://lean-lang.org/doc/reference/4.35.0/releases/v4.22.0/
Lean FRO 2026a	Lean FRO (undated, read 2026). Comparator: a trustworthy judge for Lean proofs. GitHub repository README; read by both sides	https://github.com/leanprover/comparator
Lean FRO 2026b	Lean FRO (2026-10-12). Lean 4.35.0 release notes. The Lean language reference	https://lean-lang.org/doc/reference/4.35.0/releases/v4.35.0/
Lean FRO 2026c	Lean FRO (read 2026). Error explanations, index and the page on unknownIdentifier. The Lean language reference	https://lean-lang.org/doc/reference/4.35.0/Error-Explanations/
Lean FRO 2026d	Lean FRO (read 2026). Tactic reference: exact?, apply?, simp?. The Lean language reference	https://lean-lang.org/doc/reference/4.35.0/Tactic-Proofs/Tactic-Reference/
Lee 2025	Lee, Sarkar, Tankelevitch, Drosos, Rintel, Banks, Wilson (2025). The impact of generative AI on critical thinking: self-reported reductions in cognitive effort and confidence effects from a survey of knowledge workers. CHI 2025, 1-22	https://doi.org/10.1145/3706598.3713778
Leinonen 2023	Leinonen, Hellas, Sarsa, Reeves, Denny, Prather, Becker (2023). Using large language models to enhance programming error messages. SIGCSE 2023	https://doi.org/10.1145/3545945.3569770 (arXiv:2210.11630)
Lessing 2025	Lessing, Ogbonnaya (2025). Reasoning and proof in mathematics education: a systematic literature review. Discover Education 5	https://doi.org/10.1007/s44217-025-01016-1
Li 2024b	Li, Sun, Murphy, Su, Li, Zhang, Yang, Si (2024). A survey on deep learning for theorem proving. Preprint	arXiv:2404.09939
Li 2024c	Li, Wu, Li, Wei, et al. (2024). Autoformalize mathematical statements by symbolic equivalence and semantic consistency. NeurIPS 2024	arXiv:2410.20936
Li 2026b	Li, Ammanamanchi, Bhat, Jamdar, Lin, Biderman (2026). SemantEq: faithful bidirectional equivalence of formal statements. Preprint	arXiv:2610.32919
Liang 2024c	Liang, Zhang, Cao, Wang, Ding, Yang, Vodrahalli, He, Smith, Yin, McFarland, Zou (2024). Can large language models provide useful feedback on research papers? A large-scale empirical analysis. NEJM AI 1(8); read in the preprint, arXiv 2310.01783 (v1)	https://doi.org/10.1056/AIoa2400196
Lin 2025	Lin, Tang, Lyu, Wu, et al. (2025). Goedel-Prover: a frontier model for open-source automated theorem proving. Preprint	arXiv:2502.07640
Lin 2025b	Lin, Tang, Lyu, Yang, Chung and others, with Jin (2025). Goedel-Prover-V2: scaling formal theorem proving with scaffolded data synthesis and self-correction. Preprint; the model card is Goedel-LM 2025	arXiv:2508.03613
Liu 2025b	Liu, Zheng, Lu, Cao, Yan (2025). Rethinking and improving autoformalization: towards a faithful metric and a dependency retrieval-based approach. ICLR 2025	https://dblp.org/rec/conf/iclr/LiuZLCY25
Liu 2025c	Liu, Zhu, Liu, et al. (2025). Generalized tree edit distance (GTED): a faithful evaluation metric for statement autoformalization. AI4Math workshop, ICML 2025	arXiv:2507.07399
Liu 2025d	Liu, Bao, Zhang, Liu, Chen, Liu, Jiao, Luo (2025). ATLAS: autoformalizing theorems through lifting, augmentation, and synthesis of data. NeurIPS 2025	arXiv:2502.05567
Lu 2024	Lu, Delaware, Zhang (2024). Proof automation with large language models. ASE 2024, 1509-1520	https://doi.org/10.1145/3691620.3695521 (arXiv:2409.14274)
Lu 2025	Lu, Wan, Huang, Xiong, et al. (2025). FormalAlign: automated alignment evaluation for autoformalization. ICLR 2025	arXiv:2410.10135
Lurch 2026	Lurch developers (undated, read 2026). Lurch Plus: proof verification with Lurch. Project site	https://lurch.plus/ (archived: https://web.archive.org/web/20260714221045/https://lurch.plus/)
LZ 2025a	Lean Zulip archive (2025). Machine Learning for Theorem Proving, topic Guarding against exploits in AI code, 37 messages, to 2025-08-02 (may move)	https://leanprover-community.github.io/archive/stream/219941-Machine-Learning-for-Theorem-Proving/topic/Guarding.20against.20exploits.20in.20AI.20code.html
LZ 2025b	Lean Zulip archive (2025). Machine Learning for Theorem Proving, topic Danger of Autoformalizers (e.g. Gauss), 54 messages, 2025-09-11 to 2025-11-07; met by both sides, scored by the human side (may move)	https://leanprover-community.github.io/archive/stream/219941-Machine-Learning-for-Theorem-Proving/topic/Danger.20of.20Autoformalizers.20(e.2Eg.2E.20Gauss).html
LZ 2025c	Lean Zulip archive (2025). Machine Learning for Theorem Proving, topic A (semi)-autoformalization challenge: 650=>448, 27 messages, 2025-05-16 to 2026-01-15 (may move)	https://leanprover-community.github.io/archive/stream/219941-Machine-Learning-for-Theorem-Proving/topic/A.20(semi)-autoformalization.20challenge.3A.20650.3D.3E448.html
LZ 2025d	Lean Zulip archive (2025). Machine Learning for Theorem Proving, topic on a Lean skill file for Anthropic's coding agent, 34 messages, to 2026-01-30; the exact title is in the link (may move)	https://leanprover-community.github.io/archive/stream/219941-Machine-Learning-for-Theorem-Proving/topic/Lean.20Skill.20for.20Claude.20Code.html
LZ 2025e	Lean Zulip archive (2025). general, topic TAIL - Template for AI generated Lean proofs, 10 messages, to 2025-12-31 (may move)	https://leanprover-community.github.io/archive/stream/113488-general/topic/TAIL.20-.20Template.20for.20AI.20generated.20Lean.20proofs.html
LZ 2025f	Lean Zulip archive (2025). Lean for teaching, topic Teaching with Verbose Lean, 54 messages, 2025-12-06 to 2026-02-26 (may move)	https://leanprover-community.github.io/archive/stream/187764-Lean-for-teaching/topic/Teaching.20with.20Verbose.20Lean.html
LZ 2025g	Lean Zulip archive (2025). Machine Learning for Theorem Proving, topic Wrong informal proof by AI, 15 messages, 2025-09-26 (may move)	https://leanprover-community.github.io/archive/stream/219941-Machine-Learning-for-Theorem-Proving/topic/Wrong.20informal.20proof.20by.20AI.html
LZ 2025h	Lean Zulip archive (2025). Machine Learning for Theorem Proving, topic theoretical computer science / STOC automated reviews, 4 messages, 2025-10-27 (may move)	https://leanprover-community.github.io/archive/stream/219941-Machine-Learning-for-Theorem-Proving/topic/theoretical.20computer.20science.20.2F.20STOC.20automated.20reviews.html
LZ 2026a	Lean Zulip archive (2026). general, topic AI Lean definitions, 33 messages, to 2026-02-08 (may move)	https://leanprover-community.github.io/archive/stream/113488-general/topic/AI.20Lean.20definitions.html
LZ 2026b	Lean Zulip archive (2026). Machine Learning for Theorem Proving, topic Understanding what Aristotle is formalizing, 2026-01-29; read by the formal side, not scored (may move)	https://leanprover-community.github.io/archive/stream/219941-Machine-Learning-for-Theorem-Proving/topic/Understanding.20what.20Aristotle.20is.20formalizing.html
Marceau 2011	Marceau, Fisler, Krishnamurthi (2011). Measuring the effectiveness of error messages designed for novice programmers. SIGCSE 2011, 499-504. Abstract read	https://doi.org/10.1145/1953163.1953308
Massot 2024	Massot (2024). Teaching mathematics using Lean and controlled natural language. ITP 2024, LIPIcs 309, paper 27	https://doi.org/10.4230/LIPIcs.ITP.2024.27
Massot 2026	Massot (undated, read 2026). leanblueprint: a plasTeX plugin and command-line tool for Lean blueprints. GitHub repository; held by mathematical-writing	https://github.com/PatrickMassot/leanblueprint
Massot 2026b	Massot (undated, read 2026). Verbose Lean 4: README, examples and basic configuration guide. GitHub repository; read by both sides, and the README again at the merge	https://github.com/PatrickMassot/verbose-lean4
Math Inc 2025	Math Inc (2025, undated page; September 2025 per Hales 2026). Gauss, an autoformalization agent. Company page; the owner's account	https://www.math.inc/gauss (archived: https://web.archive.org/web/20261021103654/https://www.math.inc/gauss)
Mathlib 2026	The mathlib community (undated, read 2026). Documentation style (contributor guide). Held by mathematical-writing	https://leanprover-community.github.io/contribute/doc.html
Mathlib 2026b	The mathlib community (read 2026-10-29). Mathlib statistics, section Counts. The formal side's count	https://leanprover-community.github.io/mathlib_stats.html
Mathlib Initiative 2026	Mathlib Initiative (undated, read 2026). formalization.yaml: a self-reporting standard for formalization projects. README and template	https://github.com/mathlib-initiative/formalization.yaml
MathOverflow 2026	Asker and answerers (2026-09-29). Formalization advice for mathematicians. MathOverflow question 515632; top answer by the user shown as Timothy Chow	https://mathoverflow.net/questions/515632
Matichuk 2015	Matichuk, Murray, Andronick, Jeffery, Klein, Staples (2015). Empirical study towards a leading indicator for cost of formal software verification. ICSE 2015. Paywalled	https://doi.org/10.1109/icse.2015.85
Mei 2026	Mei, Douglas (2026). Beyond LLM judge: mechanical verification for agentic autoformalization. Preprint	arXiv:2610.20573
Mensfelt 2025	Mensfelt, Tena Cucala, Franco, Koutsoukou-Argyraki, et al. (2025). Towards a common framework for autoformalization. NeLaMKRR workshop at KR 2025	arXiv:2509.09810
Mihaylova 2026	Mihaylova, Logacheva, Hellas, Fan, Castro, Akram, Norouzi, Brusilovsky, Leinonen (2026). The effects of structured LLM-generated feedback on programming assignment performance. Preprint	arXiv:2605.16933
Min 2026	Min, He, Li, et al. (2026). Theory-level autoformalization: from isolated statements to unified formal knowledge bases. Position paper, ICML 2026	arXiv:2607.13292
Mistral 2026	Mistral AI (2026-03-16). Leanstral: open-source foundation for trustworthy vibe-coding. Company news page; the owner's results	https://mistral.ai/news/leanstral (archived: https://web.archive.org/web/20261004083217/https://mistral.ai/news/leanstral/)
Mohammad 2026	Mohammad, Sheikh (2026). The faithfulness gap: certifying semantic equivalence between natural-language and formal mathematical statements. Preprint	arXiv:2606.16541
Moraru 2026	Moraru, Biswas, Gadiraju (2026). Beyond the traceback: using LLMs for adaptive explanations of programming errors. Preprint	arXiv:2608.20896
Murphy 2024	Murphy, Yang, Sun, Li, et al. (2024). Autoformalizing Euclidean geometry. ICML 2024	arXiv:2405.17216
Naproche 2026	Naproche developers (undated, read 2026). Naproche project site, and the tutorial TUTORIAL.ftl.tex	https://naproche.github.io/ ; https://github.com/naproche/naproche/blob/master/math/TUTORIAL.ftl.tex
Nipkow 2012	Nipkow (2012). Teaching semantics with a proof assistant: no more LSD trip proofs. Lecture Notes in Computer Science (2012), 24-38. Paywalled	https://doi.org/10.1007/978-3-642-27940-9_3
Numina 2025	Project Numina (2025-04-13). Kimina-Autoformalizer-7B. Model card	https://huggingface.co/project-numina/Kimina-Autoformalizer-7B
Ochigame 2024	Ochigame (2024). Automated mathematics and the reconfiguration of proof and labor. Bulletin of the AMS 61, 423-437	https://doi.org/10.1090/bull/1821
Ospanov 2025	Ospanov, Farnia, Yousefzadeh (2025). miniF2F-Lean revisited: reviewing limitations and charting a path forward. Preprint	arXiv:2511.03108
Ospanov 2025b	Ospanov, Farnia, Yousefzadeh (2025). APOLLO: automated LLM and Lean collaboration for advanced formal reasoning. NeurIPS 2025	arXiv:2505.05758
Otte 2026	Otte, Bos, Commelin, Portegies (2026). The educational proof assistant Waterproof in an introductory proof course: proof construction and learning processes. Preprint	arXiv:2606.26809
Ouvrier-Buffet 2026	Ouvrier-Buffet (2026). Mathematics teachers' practices with proof assistants: a literature review. Working paper, HAL hal-05671977	https://hal.science/hal-05671977v1
Pąk 2014	Pąk (2014). Improving legibility of natural deduction proofs is not trivial. Logical Methods in Computer Science 10(3)	https://doi.org/10.2168/LMCS-10(3:23)2014
Palomar 2026	Palomar registry (undated, read 2026). About, and Statement. Registry pages	https://palomar-registry.org/about (archived: https://web.archive.org/web/20261011082215/https://palomar-registry.org/about) ; https://palomar-registry.org/statement (archived: https://web.archive.org/web/20261011082215/https://palomar-registry.org/statement)
Palomar 2026b	Palomar registry (read 2026-10-29). Registry-wide totals, field totals of the public results API. The formal side's count, read again at the audit the same day	https://data.palomar-registry.org/api/v1/results
Parasuraman 2010	Parasuraman, Manzey (2010). Complacency and bias in human use of automation: an attentional integration. Human Factors 52(3), 381-410	https://doi.org/10.1177/0018720810376055
PASE 2022	Asker and answerers (2022-02-15). Is there a Mizar-like sublanguage for Coq? Proof Assistants Stack Exchange question 571 and its accepted answer	https://proofassistants.stackexchange.com/questions/571
PASE 2022b	Asker and answerers (2022). Examples of new mathematics discovered through formalization? Proof Assistants Stack Exchange question 129	https://proofassistants.stackexchange.com/q/129
PASE 2024	Asker and answerers (2024-06-07). Tools like leanblueprint for other proof assistants, especially Coq? Proof Assistants Stack Exchange question 4035	https://proofassistants.stackexchange.com/questions/4035
PASE 2026	Asker and answerers (2026-07-25). How can I evaluate the semantic equivalence of Lean statements generated by an autoformalization model? Proof Assistants Stack Exchange question 6608; accepted answer by the user shown as Jason Rute, who marks one mention of a prover as a plug	https://proofassistants.stackexchange.com/questions/6608
Patel 2025	Patel, Bhattacharyya, Lu, Mehta, Voss, Norouzi, Ranade (2025). LeanTutor: towards a verified AI mathematical proof tutor. Preprint	arXiv:2506.08321
Paulson 2026	Paulson (2026-01-15). Broken proofs and broken provers. Machine Logic blog	https://lawrencecpaulson.github.io/2026/01/15/Broken_proofs.html
Peng 2025	Peng, Yao, Ma, et al. (2025). CriticLean: critic-guided reinforcement learning for mathematical formalization. Preprint	arXiv:2507.06181
Perháč 2025	Perháč, Novotný, Chodarev, Kristensen, Tveito, Shturmov, Thomsen (2025). OnlineProver: experience with a visualisation tool for teaching formal proofs. ThEdu'24, EPTCS 419, 55-74	https://doi.org/10.4204/EPTCS.419.4
Perry 2023	Perry, Srivastava, Kumar, Boneh (2023). Do users write more insecure code with AI assistants? ACM CCS 2023, 2785-2799	https://doi.org/10.1145/3576915.3623157
Petrov 2025	Petrov, Dekoninck, Baltadzhiev, Drencheva, Minchev, Balunović, Jovanović, Vechev (2025). Proof or bluff? Evaluating LLMs on 2025 USA Math Olympiad. Preprint	arXiv:2503.21934
Petrov 2025b	Petrov, Dekoninck, Vechev (2025). BrokenMath: a benchmark for sycophancy in theorem proving with LLMs. Preprint	arXiv:2510.04721
Pettit 2017	Pettit, Homer, Gee (2017). Do enhanced compiler error messages help students? Results inconclusive. SIGCSE 2017, 465-470. Abstract read	https://doi.org/10.1145/3017680.3017768
Pierce 2009	Pierce (2009). Lambda, the ultimate TA: using a proof assistant to teach programming language foundations. ICFP 2009, 121-122 (invited talk abstract)	https://doi.org/10.1145/1596550.1596552
Pit-Claudel 2020	Pit-Claudel (2020). Untangling mechanized proofs. SLE 2020, 155-174. Abstract read	https://doi.org/10.1145/3426425.3426940
PNT-plus 2026	PNT+ project (read 2026). PNT+ pull request style guide, with CONTRIBUTING.md. GitHub repository	https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/blob/main/PULL_REQUEST_STYLE.md
Poiroux 2025	Poiroux, Weiss, Kunčak, Bosselut (2025). Reliable evaluation and benchmarks for statement autoformalization. EMNLP 2025, 17958-17980	https://doi.org/10.18653/v1/2025.emnlp-main.907 (arXiv:2406.07222)
Poiroux 2025b	Poiroux, Bosselut, Kunčak (2025). RLMEval: evaluating research-level neural theorem proving. Findings of EMNLP 2025	arXiv:2510.25427
Pollack 1997	Pollack (1997). How to believe a machine-checked proof. BRICS Report Series 4(18); also in Sambin, Smith (eds.), Twenty Five Years of Constructive Type Theory, Oxford University Press, 1998	https://doi.org/10.7146/brics.v4i18.18945
PostHog 2026	PostHog (read 2026). Vale and prose linting. Company handbook (may move)	https://posthog.com/handbook/wizard-and-docs/vale
Prather 2017	Prather, Pettit, McMurry, Peters, Homer, Simone, Cohen (2017). On novices' interaction with compiler error messages: a human factors approach. ICER 2017, 74-82. Abstract read	https://doi.org/10.1145/3105726.3106169
PyPI 2026	PyPI statistics (read 2026-10-29). Recent downloads of leanblueprint and lean-lsp-mcp, field last_month. The formal side's count	https://pypistats.org/api/packages/leanblueprint/recent ; https://pypistats.org/api/packages/lean-lsp-mcp/recent
Raiyan 2026	Raiyan, Kabir, Mahmud, Hasan, Ananiadou (2026). Artificial intelligence for mathematical reasoning: an integrated survey of language models, neuro-symbolic systems, and verified discovery. Preprint	arXiv:2606.08728
Rammal 2026	Rammal, Patel, Gloeckle, Hayat, Kempe, Munos, Arnal, Cabannes (2026). Formalizing mathematics at scale. Preprint; the owners' account	arXiv:2605.29955
Ranta 2026	Ranta (2026). Symbolic informalization: fluent, productive, multilingual. Preprint	arXiv:2606.16893
Rav 1999	Rav (1999). Why do we prove theorems? Philosophia Mathematica 7(1), 5-41. Paywalled	https://doi.org/10.1093/philmat/7.1.5
Ringer 2019	Ringer, Palmskog, Sergey, Gligoric, Tatlock (2019). QED at large: a survey of engineering of formally verified software. Foundations and Trends in Programming Languages 5(2-3), 102-281	https://doi.org/10.1561/2500000045 (arXiv:2003.06458)
Ringer 2020	Ringer, Sanchez-Stern, Grossman, Lerner (2020). REPLica: REPL instrumentation for Coq analysis. CPP 2020. Read in the authors' copy	https://doi.org/10.1145/3372885.3373823
Ringer 2021	Ringer, Porter, Yazdani, Leo, Grossman (2021). Proof repair across type equivalences. PLDI 2021, 112-127	https://doi.org/10.1145/3453483.3454033 (arXiv:2010.00774)
Rivin 2026	Rivin (2026-03-26). From 67% to 97%: when your theorem prover proves the wrong theorem. GitHub gist, with its benchmark repository	https://gist.github.com/igorrivin/3d15a2ba02a6ef09a5ddee196805348e (archived: https://web.archive.org/web/20260328004705/https://gist.github.com/igorrivin/3d15a2ba02a6ef09a5ddee196805348e) ; https://github.com/igorrivin/polya-szego-benchmark
Salmon 2025	Salmon, Hammer, Santos, Becker (2025). Debugging without error messages: how LLM prompting strategy affects programming error explanation effectiveness. Preprint	arXiv:2501.05706
Santos 2023	Santos, Prasad, Becker (2023). Always provide context: the effects of code context on programming error message enhancement. CompEd 2023, 147-153. Abstract read	https://doi.org/10.1145/3576882.3617909
Santos 2024	Santos, Becker (2024). Not the silver bullet: LLM-enhanced programming error messages are ineffective in practice. UKICER 2024	https://doi.org/10.1145/3689535.3689554 (arXiv:2409.18661)
Scholze 2021	Scholze (2021-06-05). Half a year of the Liquid Tensor Experiment: amazing developments. Guest post, Xena Project blog	https://xenaproject.wordpress.com/2021/06/05/half-a-year-of-the-liquid-tensor-experiment-amazing-developments/
Shen 2026	Shen, Qiu, Zhi, et al. (2026). MechAlign: evaluating semantic alignment at the project level in mathematical formalization. Preprint	arXiv:2610.35269
Song 2024	Song, Yang, Anandkumar (2024). Lean Copilot: large language models as copilots for theorem proving in Lean. NeuS 2025. The repository is LeanDojo 2026	arXiv:2404.12534
StepFun 2025	StepFun (2025-08-19). StepFun-Formalizer-32B. Model card	https://huggingface.co/stepfun-ai/StepFun-Formalizer-32B
STOC 2026	STOC 2026 organisers (2025). Experimental program: automated pre-submission feedback. Conference page (may move)	https://acm-stoc.org/stoc2026/stoc2026-LLM_feedback.html
Stylianides 2024	Stylianides, Stylianides, Moutsios-Rentzos (2024). Proof and proving in school and university mathematics education research: a systematic review. ZDM Mathematics Education 56, 47-59 (abstract read)	https://doi.org/10.1007/s11858-023-01518-y
Szegedy 2020	Szegedy (2020). A promising path towards autoformalization and general artificial intelligence. CICM 2020, Lecture Notes in Computer Science, 3-20	https://doi.org/10.1007/978-3-030-53518-6_1
Tan 2026	Tan, Blanchet, Syrgkanis (2026). PaperFormalizer: author-in-the-loop autoformalization of research papers in Lean. Preprint	arXiv:2610.31810
Tanswell 2015	Tanswell (2015). A problem with the dependence of informal proofs on formal proofs. Philosophia Mathematica 23(3), 295-310. Paywalled	https://doi.org/10.1093/philmat/nkv008
Tanswell 2026	Tanswell (2026-03-31). Vibe formalisation and slop mathematics. Talk abstract, Isaac Newton Institute	https://talks.cam.ac.uk/talk/index/245968/
Tao 2023	Tao (2023). Formalizing the proof of PFR in Lean4 using Blueprint: a short tour. Blog post; held by mathematical-writing	https://terrytao.wordpress.com/2023/11/18/formalizing-the-proof-of-pfr-in-lean4-using-blueprint-a-short-tour/
Tao 2023m	Tao (2023). Learning Lean 4, a journal in Mathstodon posts, 2023-10-09 to 2023-11-19; cited posts of 2023-10-10, 2023-10-14, 2023-10-21, 2023-11-05, 2023-11-19 (may move)	https://mathstodon.xyz/@tao/111206761117553482 ; https://mathstodon.xyz/@tao/111209438351902155 ; https://mathstodon.xyz/@tao/111234054337933006 ; https://mathstodon.xyz/@tao/111271244206606941 ; https://mathstodon.xyz/@tao/111360264941915326 ; https://mathstodon.xyz/@tao/111439273687647142
Tao 2024	Tao (2024-10-12). The equational theories project: a brief tour. Blog post	https://terrytao.wordpress.com/2024/10/12/the-equational-theories-project-a-brief-tour/
Tao 2025a	Tao (2025-05-11). Post on formalizing a one-page proof with Copilot and canonical. Mathstodon (may move)	https://mathstodon.xyz/@tao/114486537464033675
Tao 2025b	Tao (2025-10-22). Thread on Erdős problem 707, posts 2 and 3 of 3. Mathstodon (may move)	https://mathstodon.xyz/@tao/115416210007455376 ; https://mathstodon.xyz/@tao/115416211466664814
Tao 2025c	Tao (2025-11-04). Thread on vibe-coding a Lean proof for Erdős problem 613. Mathstodon (may move)	https://mathstodon.xyz/@tao/115493669248813088 ; https://mathstodon.xyz/@tao/115493672527637142
Tao 2025d	Tao (2025-12-09). The Equational Theories Project: advancing collaborative mathematical research at scale. Blog post	https://terrytao.wordpress.com/2025/12/09/the-equational-theories-project-advancing-collaborative-mathematical-research-at-scale/
Tao 2026e	Tao (2026-01-15). The integrated explicit analytic number theory network. Blog post; read by both sides	https://terrytao.wordpress.com/2026/01/15/the-integrated-explicit-analytic-number-theory-network/
Tao 2026f	Tao (2026-08-18). Palomar: a registry of Lean verified mathematics. Blog post	https://terrytao.wordpress.com/2026/08/18/palomar-a-registry-of-lean-verified-mathematics/
Tao 2026g	Tao (2026-05-04). Post on an agent triaging a referee report. Mathstodon (may move)	https://mathstodon.xyz/@tao/116517314420904580
Tao 2026h	Tao (2026-05-28). Post on skills files recording style preferences. Mathstodon (may move)	https://mathstodon.xyz/@tao/116653336847856534
Tao 2026i	Tao (2026-06-21). Thread on generation, verification and digestion in IEANTN, 3 posts. Mathstodon (may move)	https://mathstodon.xyz/@tao/116789373239346609
Tao 2026j	Tao (2026-08-12). A digestion of the proof of Sendov's conjecture. Blog post	https://terrytao.wordpress.com/2026/08/12/a-digestion-of-the-proof-of-sendovs-conjecture/
Tao 2026k	Tao (2026-01-07 to 2026-01-10). Thread on Erdős problem 728 and AI-written expositions, 5 posts and an addendum. Mathstodon (may move)	https://mathstodon.xyz/@tao/115855840223258103
Taylor 2024b	Taylor, Vassar, Renzella, Pearce (2024). dcc --help: transforming the role of the compiler by generating context-aware error explanations with large language models. SIGCSE 2024	https://doi.org/10.1145/3626252.3630822 (arXiv:2308.11873)
Thakur 2024	Thakur, Tsoukalas, Wen, Xin, Chaudhuri (2024). An in-context learning agent for formal theorem-proving (COPRA). Preprint, version 5	arXiv:2310.04353
Thoma 2022	Thoma, Iannone (2022). Learning about proof with the theorem prover LEAN: the abundant numbers task. International Journal of Research in Undergraduate Mathematics Education 8, 64-93	https://doi.org/10.1007/s40753-021-00140-1
Tran Minh 2025	Tran Minh, Gonnord, Narboux (2025). Proof assistants for teaching: a survey. arXiv preprint (abstract read)	arXiv:2505.13472
Tsoukalas 2024	Tsoukalas, Lee, Jennings, et al. (2024). PutnamBench: evaluating neural theorem-provers on the Putnam mathematical competition. NeurIPS 2024 Datasets and Benchmarks	arXiv:2407.11214
TUe 2026	Eindhoven University of Technology (undated, read 2026). Waterproof as students' personal proof assistant. DRIVE project page; no archived copy found	https://drive.tue.nl/projects/waterproof-as-students-personal-proof-assistant/
Tymoczko 1979	Tymoczko (1979). The four-color problem and its philosophical significance. The Journal of Philosophy 76(2), 57-83. Paywalled	https://doi.org/10.2307/2025976
Uskuplu 2026	Uskuplu, Moss, de Paiva (2026). KnowTeX: visualizing mathematical dependencies. arXiv preprint, version 3 (abstract read)	arXiv:2601.15294
Varambally 2025	Varambally, Voice, Sun, Chen, Yu, Ye (2025). Hilbert: recursively building formal proofs with informal reasoning. Preprint	arXiv:2509.22819
Venturim 2026	Venturim, Estrada, Silva, et al. (2026). What has actually been proved? Auditable paper-to-Lean alignment with LeanTrail. MATH-AI workshop, NeurIPS 2026	arXiv:2610.35926
Verchinine 2007	Verchinine, Lyaletski, Paskevich (2007). System for Automated Deduction (SAD): a tool for proof verification. CADE-21, LNCS 4603, 398-403	https://doi.org/10.1007/978-3-540-73595-3_29
Vergo 2026	Vergo and others (2026-02-05). Discussion thread: side-by-side blueprint. Lean community forum, public archive, channel ecosystem-infrastructure	https://leanprover-community.github.io/archive/stream/536994-ecosystem-infrastructure/topic/Discussion.20thread.20-.20Side.20by.20Side.20blueprint.html
Wang 2018	Wang, Kaliszyk, Urban (2018). First experiments with neural translation of informal to formal mathematics. CICM 2018, Lecture Notes in Computer Science, 255-270	https://doi.org/10.1007/978-3-319-96812-4_22 (arXiv:1805.06502)
Wang 2020b	Wang, Brown, Kaliszyk, Urban (2020). Exploration of neural machine translation in autoformalization of mathematics in Mizar. CPP 2020, 85-98	https://doi.org/10.1145/3372885.3373827 (arXiv:1912.02636)
Wang 2024b	Wang, Mitchell, Piech (2024). A large scale RCT on effective error messages in CS1. SIGCSE 2024, 1395-1401. Read in full through the university	https://doi.org/10.1145/3626252.3630764
Wang 2025	Wang, Unsal, Lin, Baksys, et al. (2025). Kimina-Prover preview: towards large formal reasoning models with reinforcement learning. Preprint	arXiv:2504.11354
Wang 2026	Wang, Chess, Lee, Ge, Mallavarapu, Alper, Ilin (2026). Learning to repair Lean proofs from compiler feedback. ICLR 2026 VerifAI workshop	arXiv:2602.02990
Wemmenhove 2024	Wemmenhove, Arends, Beurskens, Bhaid, McCarren, Moraal, Rivera Garrido, Tuin, Vassallo, Wils, Portegies (2024). Waterproof: educational software for learning how to write mathematical proofs. EPTCS 400, 96-119	https://doi.org/10.4204/eptcs.400.7
Weng 2025	Weng, Du, Li, Lu, Sun, Liu, Zhang (2025). Autoformalization in the era of large language models: a survey. Preprint	arXiv:2505.23486
Wenzel 1999	Wenzel (1999). Isar: a generic interpretative approach to readable formal proof documents. TPHOLs 1999, LNCS 1690, 167-183. Held by mathematical-writing	https://doi.org/10.1007/3-540-48256-3_12
Wenzel 2002	Wenzel, Wiedijk (2002). A comparison of Mizar and Isar. Journal of Automated Reasoning 29(3-4), 389-411. Title and venue only	https://doi.org/10.1023/A:1021935419355
Widjojo 2023	Widjojo, Treude (2023). Addressing compiler errors: Stack Overflow or large language models? Preprint	arXiv:2307.10793
Wiedijk 2000	Wiedijk (2000). The de Bruijn factor. Poster paper, TPHOLs 2000, with the author's page of measured factors	https://www.cs.ru.nl/~freek/factor/
Wiedijk 2004	Wiedijk (2004). Formal proof sketches. TYPES 2003, LNCS 3085, 378-393. Title and venue only	https://doi.org/10.1007/978-3-540-24849-1_24
Wiedijk 2012	Wiedijk (2012). Pollack-inconsistency. Electronic Notes in Theoretical Computer Science 285, 85-100	https://doi.org/10.1016/j.entcs.2012.06.008
Wiedijk 2012b	Wiedijk (2012). A synthesis of the procedural and declarative styles of interactive theorem proving. Logical Methods in Computer Science 8(1)	https://doi.org/10.2168/LMCS-8(1:30)2012
Wu 2022	Wu, Jiang, Li, Rabe, et al. (2022). Autoformalization with large language models. NeurIPS 2022	arXiv:2205.12615
Wu 2025b	Wu, Huang, Wan, et al. (2025). StepFun-Formalizer: unlocking the autoformalization potential of LLMs through knowledge-reasoning fusion. AAAI 2026	arXiv:2508.04440
Wu 2026	Wu (2026). Can AI review improve paper drafting? An empirical study on 20 computer architecture submissions. Preprint	arXiv:2606.01013
Xin 2024	Xin, Guo, Shao, Ren, et al. (2024). DeepSeek-Prover: advancing theorem proving in LLMs through large-scale synthetic data. Preprint	arXiv:2405.14333
Xin 2024b	Xin, Ren, Song, Shao, Zhao and others (2024). DeepSeek-Prover-V1.5: harnessing proof assistant feedback for reinforcement learning and Monte-Carlo tree search. Preprint	arXiv:2408.08152
Xu 2025	Xu, Wang, Wang, Li, Watt (2025). A minimalist proof language for neural theorem proving over Isabelle/HOL. OOPSLA 2026	arXiv:2507.18885
Yanahama 2026	Yanahama, Sannai (2026). Lean Atlas: an integrated proof environment for scalable human-AI collaborative formalization. Preprint	arXiv:2604.16347
Yang 2024	Yang, Poesia, He, Li, Lauter, Chaudhuri, Song (2024). Formal mathematical reasoning: a new frontier in AI. Position paper, preprint	arXiv:2412.16075
Ying 2024	Ying, Wu, Geng, et al. (2024). Lean Workbook: a large-scale Lean problem set formalized from natural language math problems. Preprint	arXiv:2406.03847
Yu 2025b	Yu, Peng, Ding, et al. (2025). FormalMATH: benchmarking formal mathematical reasoning of large language models. Technical report	arXiv:2505.02735
Yu 2025c	Yu, Zhong, Feng, et al. (2025). Mathesis: towards formal theorem proving from natural languages. Preprint	arXiv:2506.07047
Zhai 2024	Zhai, Wibowo, Li (2024). The effects of over-reliance on AI dialogue systems on students' cognitive abilities: a systematic review. Smart Learning Environments 11, article 28	https://doi.org/10.1186/s40561-024-00316-7
Zhang 2025	Zhang, Valentino, Meadows, Freitas (2025). Beyond gold standards: epistemic ensemble of LLM judges for formal mathematical reasoning. Preprint	arXiv:2506.10903
Zhang 2026	Zhang, Gallardo Candela, Murthy, et al. (2026). Beyond compilation: evaluating faithful natural-language-to-Lean statement formalization. Preprint, version 4	arXiv:2606.31002
Zheng 2022	Zheng, Han, Polu (2022). MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics. ICLR 2022	arXiv:2109.00110
Zheng 2023	Zheng, Wang, Xie, Liu, Sun, Xin, Shen, Li, Li (2023). Lyra: orchestrating dual correction in automated theorem proving. TMLR	arXiv:2309.15806
Zhu 2026	Zhu (undated, read 2026). LeanArchitect: generating blueprint data directly from Lean. GitHub repository README	https://github.com/hanwenzhu/LeanArchitect
Zhu 2026b	Zhu, Monticone, Welleck, Avigad (2026). LeanArchitect: automating blueprint generation for humans and AI. ITP 2026, LIPIcs 382, 25. DOI registered with DataCite; resolved through doi.org. Zhu 2026 is the tool's repository	https://doi.org/10.4230/LIPIcs.ITP.2026.25 (arXiv:2601.22554)
Joyce 1996	Joyce, D. E. (1996, from Heath's 1908 translation). Euclid's Elements, Book IX, Proposition 20, with VII.31. Clark University	https://mathcs.clarku.edu/~djoyce/java/elements/bookIX/propIX20.html
Wikipedia 2026 Euclid	Wikipedia (read 2026-11-03). Euclid's theorem, section Euclid's proof, Variations: N = n! + 1. Grey, an example only	https://en.wikipedia.org/wiki/Euclid%27s_theorem