References

A centralized bibliography for the formalizations and conjecture index in this repository. For per-conjecture details, see the linked project documentation.

Lean & Mathlib

Number Theory

General references

  • Hardy, G. H. & Wright, E. M. An Introduction to the Theory of Numbers. Oxford University Press.
  • Ireland, K. & Rosen, M. A Classical Introduction to Modern Number Theory. Springer GTM 84.
  • Guy, R. K. Unsolved Problems in Number Theory. 3rd ed., Springer, 2004.

Formalized conjectures

  • Agoh–Giuga conjecture — Agoh, T. “On Giuga’s conjecture.” Manuscripta Math. 87 (1995), 501–510. Submodule
  • Carmichael totient conjecture — Carmichael, R. D. “On Euler’s φ-function.” Bull. Amer. Math. Soc. 13 (1907), 241–243. Submodule
  • Catalan-Mersenne conjecture — Catalan-Mersenne numbers and historical conjectural remarks: Wikipedia. In-repo project
  • Collatz conjecture — Lagarias, J. C. “The 3x+1 problem and its generalizations.” Amer. Math. Monthly 92 (1985), 3–23. Submodule
  • Erdős–Straus conjecture — Erdős, P. “Az 1/x₁ + 1/x₂ + … + 1/xₙ = a/b egyenletről.” Mat. Lapok 1 (1950), 192–210. Submodule
  • Goldbach’s conjecture — Helfgott, H. A. “The ternary Goldbach conjecture is true.” arXiv:1312.7748, 2013. Submodule
  • Legendre’s conjecture — Legendre, A.-M. Essai sur la Théorie des Nombres. 2nd ed., 1808. Submodule
  • New Mersenne conjecture — Bateman, P. T.; Selfridge, J. L.; Wagstaff, S. S. Jr. and later expositions on Mersenne conjectures. Wikipedia summary. In-repo project
  • Oppermann’s conjecture — Oppermann, L. “Om vor Kundskab om Primtallenes Mængde mellem givne Grændser.” Oversigt Dansk. Vidensk. Selsk. Forh. (1882), 169–179. Submodule
  • Fortune’s conjecture — Guy, R. K. Unsolved Problems in Number Theory. 3rd ed., Springer, 2004 (Fortunate numbers section). In-repo project
    • Golomb, S. W. “A connected graph associated with the fortunate numbers.” Amer. Math. Monthly 88 (1981), 113–115.
    • Kaczorowski, J.; Szydło, B. “On the conjecture of Reo Fortune concerning certain quadratic congruences.” Math. Comp. 76 (2007), 249–258.
    • Čejchan, A.; Křížek, M.; Somer, L. “There are no sign changes in formulae involving prime numbers.” Rocky Mountain J. Math. 48 (2018), 1165–1178. (Source of primorial interval theorems formalized in Fortune.Literature.)
    • Křížek, M.; Luca, F.; Somer, L. 17 Lectures on Fermat Numbers: From Number Theory to Geometry. Springer, 2022. (Section 2.4 surveys Fortune-related primorial interval theorems.) Open chapter PDF: https://cs.uwaterloo.ca/journals/JIS/VOL25/Krizek/krizek3.pdf
    • OEIS Foundation Inc. A005235 (Fortunate numbers), with computational notes and links. https://oeis.org/A005235
  • Twin prime conjecture — de Polignac, A. “Six propositions arithmologiques déduites du crible d’Ératosthène.” Nouv. Ann. Math. 8 (1849), 423–429. Submodule

Combinatorics

General references

  • van Lint, J. H. & Wilson, R. M. A Course in Combinatorics. 2nd ed., Cambridge University Press, 2001.
  • Stanley, R. P. Enumerative Combinatorics. Vol. 1 & 2, Cambridge University Press.

Formalized conjectures

  • Dittert conjecture — N. J. Cavenagh, J. Hämäläinen, C. M. Wanless, “On Dittert’s conjecture,” Electronic Journal of Combinatorics (2008). In-repo project
  • Frankl’s union-closed sets conjecture — Poonen, B. “Union-closed families.” Journal of Combinatorial Theory, Series A 59(2), 253–268 (1992). In-repo project
    • Bruhn, H.; Schaudt, O. “The journey of the union-closed sets conjecture.” Graphs and Combinatorics 31, 2043–2074 (2015). (Survey reference for structural reductions and known partial results.)
    • Gilmer, J. “A constant lower bound for the union-closed sets conjecture.” arXiv:2211.09055, 2022. (Entropy lower bound underlying the current research/gilmer_ahs_verification.py audit.)
    • Alweiss, R.; Huang, B.; Sellke, M. “Improved lower bound for the union-closed sets conjecture.” Electronic Journal of Combinatorics 31(3), P3.35 (2024). (Sharp one-variable hinge and interval checks recorded in Frankl.AHSFormula, Frankl.AHSData, and Frankl.AHSInterval.)
    • Vučković, B.; Živković, M. “Formalizing Frankl’s Conjecture: FC-families.” arXiv:1207.3604, 2012. (For the singleton FC-family viewpoint formalized in Frankl.Basic.)
  • 1/3–2/3 conjecture — Kislitsyn, S. S. “Finite partially ordered sets and their associated sets of permutations.” Matematicheskie Zametki 4 (1968), 511–518. In-repo project
    • Fredman, M. L. “How good is the information theory bound in sorting?” Theoret. Comput. Sci. 1 (1976), 355–361. (Independent statement; the sorting/merging motivation.)
    • Linial, N. “The information-theoretic bound is good for merging.” SIAM J. Comput. 13 (1984), 795–801. (Width-2 case and tightness of 1/3 — see Width2 and SmallCases.V3_balance_tight.)
    • Kahn, J.; Saks, M. “Balancing poset extensions.” Order 1 (1984), 113–126. (First constant bound δ(P) ≥ 3/11 ≈ 0.273.)
    • Brightwell, G.; Felsner, S.; Trotter, W. T. “Balancing pairs and the cross product conjecture.” Order 12 (1995), 327–349. (Current record δ(P) ≥ (5−√5)/10 ≈ 0.2764, via Ahlswede–Daykin/FKG.)
    • Brightwell, G. “Balanced pairs in partial orders.” Discrete Math. 201 (1999), 25–52. (Survey; semiorder case.)
    • Sah, A. “Improving the 1/3–2/3 Conjecture for Width Two Posets.” Combinatorica 41 (2021), 99–126. arXiv:1811.01500. (Width-2 constant ≈ 0.3388; families with δ → ≈ 0.3488.)
  • Gold partition conjecture — M. Peczarski, “The Gold Partition Conjecture,” Order 29 (2012), 321–336. In-repo project
  • Hadamard conjecture — Hadamard, J. “Résolution d’une question relative aux déterminants.” Bull. Sci. Math. 17 (1893), 240–246. Submodule
  • Sensitivity conjecture (now theorem) — Huang, H. “Induced subgraphs of hypercubes and a proof of the Sensitivity Conjecture.” Ann. of Math. 190 (2019), 949–955. Submodule
  • Singmaster’s conjecture — Singmaster, D. “How often does an integer occur as a binomial coefficient?” Amer. Math. Monthly 78 (1971), 385–386. In-repo project
    • Abbott, H. L.; Erdős, P.; Hanson, D. “On the number of times an integer occurs as a binomial coefficient.” Amer. Math. Monthly 81 (1974), 256–261. (Bound O(log a / log log a).)
    • Kane, D. M. “Improved bounds on the number of ways of expressing t as a binomial coefficient.” Integers 7 (2007), A53. (Sharpest known upper bound.)

Algebra

General references

  • Lang, S. Algebra. Revised 3rd ed., Springer GTM 211.
  • Rotman, J. J. An Introduction to the Theory of Groups. 4th ed., Springer GTM 148.

Formalized conjectures

  • Herzog–Schönheim conjecture — Herzog, M. & Schönheim, J. “Research problem No. 9.” Canad. Math. Bull. 17 (1974), 150. Submodule

Graph Theory

General references

  • Diestel, R. Graph Theory. 5th ed., Springer GTM 173, 2017.
  • Bondy, J. A. & Murty, U. S. R. Graph Theory. Springer GTM 244, 2008.

Formalized conjectures

  • Reconstruction conjecture — Kelly, P. J. “A congruence theorem for trees.” Pacific J. Math. 7 (1957), 961–968. Ulam, S. M. A Collection of Mathematical Problems. Interscience, 1960. Submodule
  • Tuza’s conjecture — Tuza, Zs. “Conjecture.” In Finite and Infinite Sets (Proc. Colloq. Math. Soc. János Bolyai), 1981. In-repo project
    • Tuza, Zs. “A conjecture on triangles of graphs.” Graphs and Combinatorics 6 (1990), 373–380. (Planar case.)
    • Krivelevich, M. “On a conjecture of Tuza about packing and covering of triangles.” Discrete Math. 142 (1995), 281–286. (Fractional version τ* ≤ 2ν*.)
    • Haxell, P. E. “Packing and covering triangles in graphs.” Discrete Math. 195 (1999), 251–254. (Best known bound τ ≤ (3 − 3/23)ν.)

General Problem Collections

  • Guy, R. K. Unsolved Problems in Number Theory. 3rd ed., Springer, 2004.
  • Croft, H. T.; Falconer, K. J. & Guy, R. K. Unsolved Problems in Geometry. Springer, 1991.
  • Wikipedia. List of conjectures.