HEXAGONbeta

Linchpin Theorems

Primarily AI-generated textHuman understanding: some partsmath.GM — General Mathematics

Contributed by Thomas Hales ↗

Version 1 / Oct 16, 2026 / CC BY 4.0

Abstract

A proof assistant checks a formal proposition. It does not check that the proposition expresses the mathematics that its author intended. This distinction becomes pressing when large bodies of mathematics are autoformalized. We propose the use of linchpin theorems: statements whose meanings can be audited with relatively little mathematical infrastructure, and whose proofs connect them to substantial results. Examples range from sphere packing and the classification of Lie algebras to regularity theory, the Weil conjectures, and computational complexity.

Provenance statement

ChatGPT-6 Astra generated this document at the prompting of Thomas Hales. There is no human authorship.

References

  1. F. J. Almgren, Jr., Almgren's Big Regularity Paper: QQ-Valued Functions Minimizing Dirichlet's Integral and the Regularity of Area-Minimizing Rectifiable Currents up to Codimension 2 , edited by V. Scheffer and J. E. Taylor, World Scientific Monograph Series in Mathematics, vol. 1, World Scientific, 2000.
  2. L. Ambrosio, N. Fusco, and D. Pallara, Functions of Bounded Variation and Free Discontinuity Problems , Oxford Mathematical Monographs, Oxford University Press, 2000. 10.1093/oso/9780198502456.001.0001.DOI
  3. J. Araújo, W. Bentz, and P. J. Cameron, The existential transversal property: a generalization of homogeneity and its impact on semigroups, Trans. Amer. Math. Soc. 374 (2021), 1155--1195. 10.1090/tran/8285.DOI
  4. L. Báez-Duarte, A strengthening of the Nyman--Beurling criterion for the Riemann hypothesis, Rend. Lincei Mat. Appl. (9) 14 (2003), 5--11. math/0202141 .
  5. B. Bagchi, On Nyman, Beurling and Baez-Duarte's Hilbert space reformulation of the Riemann hypothesis, Proc. Indian Acad. Sci. Math. Sci. 116 (2006), 137--146. 10.1007/BF02829783.DOI
  6. T. Barnet-Lamb, D. Geraghty, M. Harris, and R. Taylor, A family of Calabi--Yau varieties and potential automorphy II, Publ. Res. Inst. Math. Sci. 47 (2011), 29--98. 10.2977/PRIMS/31.DOI
  7. A. Beurling, A closure problem related to the Riemann zeta-function, Proc. Natl. Acad. Sci. USA 41 (1955), 312--314. 10.1073/pnas.41.5.312.DOI
  8. B. J. Birch, Conjectures concerning elliptic curves, in Arithmetic Algebraic Geometry , Proc. Sympos. Pure Math., vol. 8, American Mathematical Society, 1965, pp. 106--112.
  9. B. J. Birch and H. P. F. Swinnerton-Dyer, Notes on elliptic curves. I, J. Reine Angew. Math. 212 (1963), 7--25. 10.1515/crll.1963.212.7.DOI
  10. B. J. Birch and H. P. F. Swinnerton-Dyer, Notes on elliptic curves. II, J. Reine Angew. Math. 218 (1965), 79--108. 10.1515/crll.1965.218.79.DOI
Show all 68 referencesShow fewer references
  1. A. Borel, Some remarks about Lie groups transitive on spheres and tori, Bull. Amer. Math. Soc. 55 (1949), 580--587. 10.1090/S0002-9904-1949-09251-0.DOI
  2. A. Borisov, Quotient singularities, integer ratios of factorials, and the Riemann hypothesis, Int. Math. Res. Not. 2008 , article rnn052. 10.1093/imrn/rnn052.DOI
  3. C. Breuil, B. Conrad, F. Diamond, and R. Taylor, On the modularity of elliptic curves over \(\Q\): wild 33-adic exercises, J. Amer. Math. Soc. 14 (2001), 843--939.
  4. M. R. Bridson and A. Haefliger, Metric Spaces of Non-Positive Curvature , Grundlehren der mathematischen Wissenschaften, vol. 319, Springer, 1999. 10.1007/978-3-662-12494-9.DOI
  5. P. J. Cameron, Permutation Groups , London Mathematical Society Student Texts, vol. 45, Cambridge University Press, 1999.
  6. A. Chambolle, L. A. D. Ferrari, and B. Merlet, Strong approximation in hh-mass of rectifiable currents under homological constraint, Adv. Calc. Var. 14 (2021), 343--363. 10.1515/acv-2018-0079.DOI
  7. J. Coates and A. Wiles, On the conjecture of Birch and Swinnerton-Dyer, Invent. Math. 39 (1977), 223--251. 10.1007/BF01402975.DOI
  8. K. Conrad, Partial Euler products on the critical line, Canad. J. Math. 57 (2005), 267--297. 10.4153/CJM-2005-012-6.DOI
  9. S. A. Cook, The complexity of theorem-proving procedures, in Proceedings of the Third Annual ACM Symposium on Theory of Computing , ACM, 1971, pp. 151--158. 10.1145/800157.805047.DOI
  10. D. A. Cox, Primes of the Form x2+ny2x^2+ny^2: Fermat, Class Field Theory, and Complex Multiplication , second ed., Wiley, 2013.
  11. A. J. de Jong, Smoothness, semi-stability and alterations, Publ. Math. Inst. Hautes Études Sci. 83 (1996), 51--93. 10.1007/BF02698644.DOI
  12. A. J. de Jong, Families of curves and alterations, Ann. Inst. Fourier (Grenoble) 47 (1997), 599--621. 10.5802/aif.1575.DOI
  13. P. Deligne, La conjecture de Weil. I, Publ. Math. Inst. Hautes Études Sci. 43 (1974), 273--307. Numdam (https://www.numdam.org/item/PMIHES_1974__43__273_0/).link
  14. P. Deligne, La conjecture de Weil. II, Publ. Math. Inst. Hautes Études Sci. 52 (1980), 137--252. Numdam (https://www.numdam.org/item/PMIHES_1980__52__137_0/).link
  15. H. Federer, Geometric Measure Theory , Grundlehren der mathematischen Wissenschaften, vol. 153, Springer, 1969.
  16. B. Fein, W. M. Kantor, and M. Schacher, Relative Brauer groups. II, J. Reine Angew. Math. 328 (1981), 39--57. 10.1515/crll.1981.328.39.DOI
  17. M. R. Garey, D. S. Johnson, and L. Stockmeyer, Some simplified NP-complete graph problems, Theoret. Comput. Sci. 1 (1976), 237--267. 10.1016/0304-3975(76)90059-1.DOI
  18. R. Ghiloni and E. Savi, The Nash--Tognoli theorem over the rationals and its version for isolated singularities, preprint, 2023, revised 2025. 2302.04142v4 .
  19. S. R. Ghorpade and G. Lachaud, Étale cohomology, Lefschetz theorems and number of points of singular varieties over finite fields, Mosc. Math. J. 2 (2002), 589--631; corrected version, 0808.2169 .
  20. D. Goldfeld, Sur les produits partiels eulériens attachés aux courbes elliptiques, C. R. Acad. Sci. Paris Sér. I Math. 294 (1982), 471--474.
  21. T. C. Hales, The work of Ngô Bao Châu, Notices Amer. Math. Soc. 58 (2011), 453--458. 1012.0382 .
  22. T. Hales, M. Adams, G. Bauer, T. D. Dang, J. Harrison, L. T. Hoang, C. Kaliszyk, V. Magron, S. McLaughlin, T. T. Nguyen, Q. T. Nguyen, T. Nipkow, S. Obua, J. Pleso, J. Rute, A. Solovyev, T. H. A. Ta, N. T. Tran, T. D. Trieu, J. Urban, K. Vu, and R. Zumkeller, A formal proof of the Kepler conjecture, Forum Math. Pi 5 (2017), e2, 29 pp. 10.1017/fmp.2017.1.DOI
  23. M. Harris, N. Shepherd-Barron, and R. Taylor, A family of Calabi--Yau varieties and potential automorphy, Ann. of Math. (2) 171 (2010), 779--813. 10.4007/annals.2010.171.779.DOI
  24. M. J. H. Heule, Schur number five, in Proceedings of the AAAI Conference on Artificial Intelligence , vol. 32, 2018, pp. 6598--6606. 10.1609/aaai.v32i1.12209.DOI
  25. M. J. H. Heule, O. Kullmann, and V. W. Marek, Solving and verifying the Boolean Pythagorean triples problem via cube-and-conquer, in Theory and Applications of Satisfiability Testing---SAT 2016 , Lecture Notes in Computer Science, vol. 9710, Springer, 2016, pp. 228--245. 10.1007/978-3-319-40970-2_15.DOI
  26. J. E. Humphreys, Introduction to Lie Algebras and Representation Theory , Graduate Texts in Mathematics, vol. 9, Springer, 1972.
  27. A. W. Knapp, Lie Groups Beyond an Introduction , second ed., Progress in Mathematics, vol. 140, Birkhäuser, 2002.
  28. J. C. Lagarias, An elementary problem equivalent to the Riemann hypothesis, Amer. Math. Monthly 109 (2002), 534--543. 10.1080/00029890.2002.11919883.DOI
  29. G. Laumon and B.-C. Ngô, Le lemme fondamental pour les groupes unitaires, Ann. of Math. (2) 168 (2008), 477--573. 10.4007/annals.2008.168.477.DOI
  30. J. E. Littlewood, Quelques conséquences de l'hypothèse que la fonction ζ(s)\zeta(s) de Riemann n'a pas de zéros dans le demi-plan ℜs>1/2\Re s>1/2, C. R. Acad. Sci. Paris 154 (1912), 263--266.
  31. K. Madlener, S. Smetsers, and M. van Eekelen, A formal verification study on the Rotterdam storm surge barrier, in Formal Methods and Software Engineering---ICFEM 2010 , Lecture Notes in Computer Science, vol. 6447, Springer, 2010, pp. 287--302. 10.1007/978-3-642-16901-4_20.DOI
  32. J. Milnor, Morse Theory , Annals of Mathematics Studies, vol. 51, Princeton University Press, 1963.
  33. N. I. S. Mohammad and T. Sheikh, The faithfulness gap: certifying semantic equivalence between natural-language and formal mathematical statements, preprint, 2026. 2606.16541 .
  34. E. E. Moise, Geometric Topology in Dimensions 2 and 3 , Graduate Texts in Mathematics, vol. 47, Springer, 1977.
  35. J. Morgan and G. Tian, Ricci Flow and the Poincaré Conjecture , Clay Mathematics Monographs, vol. 3, American Mathematical Society and Clay Mathematics Institute, 2007.
  36. T. Neary and D. Woods, P-completeness of cellular automaton Rule 110, in Automata, Languages and Programming---ICALP 2006 , Lecture Notes in Computer Science, vol. 4051, Springer, 2006, pp. 132--143. 10.1007/11786986_13.DOI
  37. B.-C. Ngô, Le lemme fondamental pour les algèbres de Lie, Publ. Math. Inst. Hautes Études Sci. 111 (2010), 1--169. 10.1007/s10240-010-0026-7.DOI
  38. B. Nyman, On Some Groups and Semigroups of Translations , doctoral thesis, Uppsala University, 1950.
  39. B. O'Neill, Semi-Riemannian Geometry with Applications to Relativity , Pure and Applied Mathematics, vol. 103, Academic Press, 1983.
  40. G. Perelman, The entropy formula for the Ricci flow and its geometric applications, preprint, 2002. math/0211159 .
  41. G. Perelman, Ricci flow with surgery on three-manifolds, preprint, 2003. math/0303109 .
  42. G. Perelman, Finite extinction time for the solutions to the Ricci flow on certain three-manifolds, preprint, 2003. math/0307245 .
  43. R. Pollack, How to believe a machine-checked proof, in G. Sambin and J. Smith (eds.), Twenty Five Years of Constructive Type Theory , Oxford University Press, 1998, pp. 205--220. Preprint: BRICS Report RS-97-18, 1997, 10.7146/brics.v4i18.18945.DOI
  44. M. Rapoport and T. Zink, Über die lokale Zetafunktion von Shimuravarietäten. Monodromiefiltration und verschwindende Zyklen in ungleicher Charakteristik, Invent. Math. 68 (1982), 21--101. 10.1007/BF01394268.DOI
  45. Yu. G. Reshetnyak, The weak convergence of completely additive vector-valued set functions, Siberian Math. J. 9 (1968), 1039--1045. 10.1007/BF02196453.DOI
  46. G. Robin, Grandes valeurs de la fonction somme des diviseurs et hypothèse de Riemann, J. Math. Pures Appl. (9) 63 (1984), 187--213.
  47. J. Rushby, Formal Methods and their Role in the Certification of Critical Systems , Technical Report SRI-CSL-95-1, Computer Science Laboratory, SRI International, 1995. Also issued as NASA Contractor Report 4673 under the title Formal Methods and Their Role in Digital Systems Validation for Airborne Systems . NASA report (https://ntrs.nasa.gov/citations/19960008816).link
  48. A. J. Scholl, Hypersurfaces and the Weil conjectures, Int. Math. Res. Not. 2011 , no. 5, 1010--1022. 10.1093/imrn/rnq098.DOI
  49. F. Schulze, Optimal isoperimetric inequalities for surfaces in any codimension in Cartan--Hadamard manifolds, Geom. Funct. Anal. 30 (2020), 255--288. 10.1007/s00039-020-00522-8.DOI
  50. J. H. Silverman, The Arithmetic of Elliptic Curves , second ed., Graduate Texts in Mathematics, vol. 106, Springer, 2009.
  51. J. H. Silverman, Advanced Topics in the Arithmetic of Elliptic Curves , Graduate Texts in Mathematics, vol. 151, Springer, 1994.
  52. A. R. Smith III, Real-time language recognition by one-dimensional cellular automata, J. Comput. System Sci. 6 (1972), 233--253. 10.1016/S0022-0000(72)80004-7.DOI
  53. K. Soundararajan, Partial sums of the Möbius function, J. Reine Angew. Math. 631 (2009), 141--152. 10.1515/CRELLE.2009.044.DOI
  54. A. Topaz, Definitions in the liquid tensor experiment, Lean community blog , 14 October 2022. Online article (https://leanprover-community.github.io/blog/posts/lte-examples/).link
  55. J. B. Tunnell, A classical Diophantine problem and modular forms of weight 3/23/2, Invent. Math. 72 (1983), 323--334. 10.1007/BF01389327.DOI
  56. J.-L. Waldspurger, Sur les coefficients de Fourier des formes modulaires de poids demi-entier, J. Math. Pures Appl. (9) 60 (1981), 375--484.
  57. J.-L. Waldspurger, Endoscopie et changement de caractéristique, J. Inst. Math. Jussieu 5 (2006), 423--525.
  58. Y. Wu, A. Q. Jiang, W. Li, M. N. Rabe, C. Staats, M. Jamnik, and C. Szegedy, Autoformalization with large language models, Advances in Neural Information Processing Systems 35 (2022), 32353--32368. 2205.12615 .

Version history

  1. v1Submitted by Thomas HalesInitial depositCurrentOct 16, 2026