References
IEEE-numbered reference list for the final report. This is the single source of truth: section files cite as [N] where N matches the number below. Obsidian will handle PDF / LaTeX export at submission time - no Pandoc or external bibliography tool is in the loop.
Sources [1]–[12] are the originally-submitted Research Plan bibliography. [13]–[14] were added after the 2026-01 pivot to support the toy-assistant implementation chapters. [15]–[17] were added during the 2026-04 restructure to back the AI-inflection (§4) and defence-in-depth (§2) framing.
[1] M. Ayala-Rincón and F. L. C. de Moura, Applied Logic for Computer Scientists: Computational Deduction and Formal Proofs, Springer, 2017.
[2] H. Geuvers, “Proof assistants: history, ideas and future,” Sadhana, vol. 34, pp. 3–25, 2009.
[3] L. C. Paulson, “A machine-assisted proof of Gödel’s incompleteness theorems for the theory of hereditarily finite sets,” Review of Symbolic Logic, vol. 7, no. 3, pp. 484–498, 2014.
[4] E. Mendelson, Introduction to Mathematical Logic, 6th ed., CRC Press, 2015.
[5] L. de Moura, S. Kong, J. Avigad, F. van Doorn, and J. von Raumer, “The Lean theorem prover (system description),” in 25th International Conference on Automated Deduction (CADE-25), Berlin, Germany, 2015.
[6] Y. Bertot and P. Castéran, Interactive Theorem Proving and Program Development: Coq’Art – The Calculus of Inductive Constructions, Springer, 2004.
[7] G. Gonthier, A. Asperti, J. Avigad, Y. Bertot, C. Cohen, F. Garillot, S. Le Roux, A. Mahboubi, R. O’Connor, S. O. Biha, I. Pasca, L. Rideau, A. Solovyev, E. Tassi, and L. Théry, “A machine-checked proof of the odd order theorem,” in Interactive Theorem Proving (ITP 2013), LNCS 7998, 2012.
[8] G. Gonthier, “A computer-checked proof of the four colour theorem,” in Handbook of the History of Logic, Vol. 9: Computational Logic, Elsevier, 2012.
[9] R. P. Nederpelt and H. Geuvers, Type Theory and Formal Proof: An Introduction, 2nd ed., Cambridge University Press, 2023.
[10] T. Tao, T. Gowers, B. Green, and F. Manners, “Marton’s Polynomial Freiman-Ruzsa conjecture,” preprint, 2024. [Online]. Available: https://teorth.github.io/pfr/
[11] G. Lowe, “Breaking and fixing the Needham-Schroeder public-key protocol using CSP and FDR,” in Tools and Algorithms for the Construction and Analysis of Systems (TACAS ‘96), 1995.
[12] B. Smyth, “Formal verification of cryptographic protocols,” Ph.D. dissertation, University of Birmingham, 2011.
[13] B. C. Pierce, Types and Programming Languages, MIT Press, 2002.
[14] R. Harper, Practical Foundations for Programming Languages, 2nd ed., Cambridge University Press, 2016.
[15] T. H. Trinh, Y. Wu, Q. V. Le, H. He, and T. Luong, “Solving olympiad geometry without human demonstrations,” Nature, vol. 625, no. 7995, pp. 476-481, 2024.
[16] P. Song, K. Yang, and A. Anandkumar, “Lean Copilot: Large language models as copilots for theorem proving in Lean,” arXiv preprint arXiv:2404.12534, 2024.
[17] N. G. Leveson and C. S. Turner, “An investigation of the Therac-25 accidents,” Computer, vol. 26, no. 7, pp. 18-41, 1993.