Optimization constants
The 5 problem files in FormalConjectures/OptimizationConstants that state a research or textbook statement, at commit 2055e5ad, one article each.
Their docstrings and Lean statements are quoted from Formal Conjectures (Google DeepMind) at that commit, under its Apache-2.0 license.
TheoremTao's Optimization constant 1a / An autocorrelation constant related to Sidon sets#
References: - Tao's optimization constant 1a - [M2010] Matolcsi, Máté, and Carlos Vinuesa. "Improved bounds on the supremum of autoconvolutions." Journal of mathematical analysis and applications 372.2 (2010): 439-447. arXiv:0907.1379 - [Y2026] Yuksekgonul, Mert et al., "Learning to Discover at Test Time," 2026, arXiv:2601.16175 - [T2026] Together AI, "EinsteinArena-new-SOTA: State-of-the-art results on open math problems," 2026, GitHub - [PBV2026] Piterbarg, Andrei, Jai Bajaj, and Derrick Vincent. "A multi-scale arcsine lower bound for the Sidon autocorrelation constant \(C_{1a}\)," 2026, GitHub
Quoted from FormalConjectures/OptimizationConstants/1a.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The file states 5 research or textbook statements: 3 open and 2 solved.
Constant1a.c1a_lower_bound
Solved: stated here without proof.
A lower bound, proven by Matolcsi-Vinuesa in [M2010].
theorem c1a_lower_bound : 1.2748 ≤ C1a
Category research solved; AMS 05 Combinatorics, 11 Number theory, 26 Real functions. Declared in FormalConjectures/OptimizationConstants/1a.lean, line 58.
Constant1a.c1a_upper_bound
Solved: stated here without proof.
An upper bound, proven by Yuksekgonul et al. in [Y2026].
theorem c1a_upper_bound : C1a ≤ 1.5029
Category research solved; AMS 05 Combinatorics, 11 Number theory, 26 Real functions. Declared in FormalConjectures/OptimizationConstants/1a.lean, line 63.
Constant1a.mem_Ico_c1a
Open: stated without proof.
How can the best known upper bound \(1.5028628587\ldots\) of [T2026] be improved?
The step function published with [T2026] gives \(1.50286285870\ldots\). The figure \(1.502862\) in the table of the first reference is this value truncated, so it is not a known upper bound.
theorem mem_Ico_c1a : mem_Ico_c1a.answer ∈ Set.Ico C1a 1.5028628587
Category research open; AMS 05 Combinatorics, 11 Number theory, 26 Real functions. Declared in FormalConjectures/OptimizationConstants/1a.lean, line 73.
Constant1a.mem_Ioc_c1a
Open: stated without proof.
How can the best known lower bound \(1.292\) of [PBV2026] be improved?
theorem mem_Ioc_c1a : mem_Ioc_c1a.answer ∈ Set.Ioc 1.292 C1a
Category research open; AMS 05 Combinatorics, 11 Number theory, 26 Real functions. Declared in FormalConjectures/OptimizationConstants/1a.lean, line 80.
Constant1a.c1a_eq
Open: stated without proof.
What is the exact value of the constant?
theorem c1a_eq : C1a = c1a_eq.answer
Category research open; AMS 05 Combinatorics, 11 Number theory, 26 Real functions. Declared in FormalConjectures/OptimizationConstants/1a.lean, line 87.
Sources
TheoremTao's Optimization Constant 6a / The Union-Closed Sets Conjecture#
References: - Tao's Optimization Constant 6a - [F1995] Frankl, P., Extremal set systems. Handbook of Combinatorics (1995). - [AHS2022] Alweiss, R., Huang, B. and Sellke, M., Improved lower bound for the union-closed sets conjecture. arXiv:2211.11731 - [CL2022] Chase, Z. and Lovett, S., Approximate union closed conjecture. arXiv:2211.11689 - [S2022] Sawin, W., An improved lower bound for the union-closed set conjecture. arXiv:2211.11504 - [C2022] Cambie, S., Better bounds for the union-closed sets conjecture using the entropy approach. arXiv:2212.12500 - [Y2022] Yu, L., Dimension-free bounds for the union-closed sets conjecture. arXiv:2212.00658 - [L2023] Liu, J., Improving the lower bound for the union-closed sets conjecture via conditionally IID coupling. arXiv:2306.08824
Quoted from FormalConjectures/OptimizationConstants/6a.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The file states 7 research or textbook statements: 3 open and 4 solved.
Constant6a.c6a_eq_half
Open: stated without proof.
The union-closed sets conjecture of Frankl: \(C_{6a} = 1/2\).
theorem c6a_eq_half : C6a = 1 / 2
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/OptimizationConstants/6a.lean, line 56.
Constant6a.c6a_upper_bound
Solved: stated here without proof.
The upper bound \(C_{6a} \le 1/2\) [F1995]. It holds because in the family of all subsets of a finite set, every element belongs to exactly half of the sets.
theorem c6a_upper_bound : C6a ≤ 1 / 2
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/OptimizationConstants/6a.lean, line 62.
Constant6a.c6a_upper_bound_improved
Open: stated without proof.
Can the best known upper bound \(1/2\) be improved?
theorem c6a_upper_bound_improved : C6a < 1 / 2
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/OptimizationConstants/6a.lean, line 67.
Constant6a.c6a_lower_bound_first
Solved: stated here without proof.
The first lower bound, \((3 - \sqrt 5) / 2\), proved independently in [AHS2022], [CL2022] and [S2022].
theorem c6a_lower_bound_first : (3 - Real.sqrt 5) / 2 ≤ C6a
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/OptimizationConstants/6a.lean, line 73.
Constant6a.c6a_lower_bound_intermediate
Solved: stated here without proof.
An intermediate lower bound, proved in [C2022] and [Y2022].
theorem c6a_lower_bound_intermediate : 0.38234 ≤ C6a
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/OptimizationConstants/6a.lean, line 78.
Constant6a.c6a_lower_bound
Solved: stated here without proof.
The best known lower bound, proved by Liu in [L2023].
theorem c6a_lower_bound : 0.38271 ≤ C6a
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/OptimizationConstants/6a.lean, line 83.
Constant6a.c6a_lower_bound_improved
Open: stated without proof.
Can the best known lower bound \(0.38271\) of [L2023] be improved?
theorem c6a_lower_bound_improved : 0.38272 < C6a
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/OptimizationConstants/6a.lean, line 88.
Sources
TheoremTao's Optimization Constant 7a / The Irrationality Measure of \(\pi\)#
References: - Tao's Optimization Constant 7a - [D1842] Dirichlet, L. G. P., Verallgemeinerung eines Satzes aus der Lehre von den Kettenbrüchen nebst einigen Anwendungen auf die Theorie der Zahlen. Sitzungsberichte der Preussischen Akademie der Wissenschaften (1842), 93–95. - [M1953] Mahler, K., On the approximation of \(\pi\). Nederl. Akad. Wetensch. Proc. Ser. A 56 = Indag. Math. 15 (1953), 30–42. - [R1955] Roth, K. F., Rational approximations to algebraic numbers. Mathematika 2 (1955), 1–20. - [RV1993] Rhin, G. and Viola, C., On the irrationality measure of \(\zeta(2)\). Ann. Inst. Fourier 43 (1993), 85–109. - [ZZ2020] Zeilberger, D. and Zudilin, W., The irrationality measure of \(\pi\) is at most \(7.103205334137\ldots\). Moscow J. Comb. Number Theory 9 (2020), 407–419. arXiv:1912.06345 - [OAI2026] OpenAI, The irrationality exponent of \(\pi\) is 2, 2026.
Quoted from FormalConjectures/OptimizationConstants/7a.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The file states 7 research or textbook statements: 5 solved and 2 textbook results. It also has 3 API statements, counted here but not shown.
Constant7a.two_le_irrationalityExponent
Textbook result, stated without proof.
Every irrational real number has irrationality exponent at least two by Dirichlet's approximation theorem [D1842].
theorem two_le_irrationalityExponent {x : ℝ} (hx : Irrational x) :
2 ≤ irrationalityExponent x
Category textbook; AMS 11 Number theory. Declared in FormalConjectures/OptimizationConstants/7a.lean, line 98.
Constant7a.irrationalityExponent_of_algebraic
Solved: stated here without proof.
Every algebraic real number has irrationality exponent at most two. For irrational algebraic numbers, this is Roth's theorem [R1955].
theorem irrationalityExponent_of_algebraic {x : ℝ} (hx : IsAlgebraic ℚ x) :
irrationalityExponent x ≤ 2
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OptimizationConstants/7a.lean, line 105.
Constant7a.c7a_lower_bound
Textbook result, proved here.
The sharp lower bound, given by Dirichlet's theorem [D1842]. This bound holds for every irrational real number.
theorem c7a_lower_bound : 2 ≤ C7a
Category textbook; AMS 11 Number theory. Declared in FormalConjectures/OptimizationConstants/7a.lean, line 116.
Constant7a.c7a_le_42
Solved: stated here without proof.
The first known upper bound, proved by Mahler in [M1953]. This was the first proof that \(C_{7a}\) is finite, or equivalently that \(\pi\) is not a Liouville number.
theorem c7a_le_42 : C7a ≤ 42
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OptimizationConstants/7a.lean, line 121.
Constant7a.c7a_lt_14_797075
Solved: stated here without proof.
An intermediate upper bound proved by Rhin and Viola in [RV1993]. It follows from an effective irrationality measure for \(\zeta(2) = \pi^2 / 6\).
theorem c7a_lt_14_797075 : C7a < 14.797075
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OptimizationConstants/7a.lean, line 127.
Constant7a.c7a_upper_bound
Solved: stated here without proof.
The best upper bound before [OAI2026], proved by Zeilberger and Zudilin in [ZZ2020].
theorem c7a_upper_bound : C7a < 7.103205334138
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OptimizationConstants/7a.lean, line 132.
Constant7a.c7a_eq_two
Solved: stated here; a Lean proof is at https://github.com/openai/math/blob/main/lean/ComparatorChallenges/PiExponent.lean.
The irrationality measure of \(\pi\) is exactly \(2\), proved by OpenAI in [OAI2026].
theorem c7a_eq_two : C7a = 2
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OptimizationConstants/7a.lean, line 139.
Sources
TheoremTao's Optimization Constant 7b / The Irrationality Measure of \(\Gamma(1/4)\)#
References: - Tao's Optimization Constant 7b - [D1842] Dirichlet, L. G. P., Verallgemeinerung eines Satzes aus der Lehre von den Kettenbrüchen nebst einigen Anwendungen auf die Theorie der Zahlen. Sitzungsberichte der Preussischen Akademie der Wissenschaften (1842), 93–95. - [C1976] Chudnovsky, G. V., Algebraic independence of constants connected with the exponential and the elliptic functions. Dokl. Akad. Nauk Ukrain. SSR Ser. A 1976, no. 8, 698–701. - [Bru2002] Bruiltet, S., D'une mesure d'approximation simultanée à une mesure d'irrationalité : le cas de \(\Gamma(1/4)\) et \(\Gamma(1/3)\). Acta Arith. 104 (2002), 243–281.
Quoted from FormalConjectures/OptimizationConstants/7b.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The file states 5 research or textbook statements: 2 open and 3 solved.
Constant7b.irrational_gamma_one_div_four
Solved: stated here without proof.
\(\Gamma(1/4)\) is irrational, as proven in [C1976].
theorem irrational_gamma_one_div_four : Irrational (Real.Gamma (1 / 4))
Category research solved; AMS 11 Number theory, 33 Special functions. Declared in FormalConjectures/OptimizationConstants/7b.lean, line 49.
Constant7b.c7b_lower_bound
Proved here.
The first and current best known lower bound, given by Dirichlet's theorem [D1842]. It applies because \(\Gamma(1/4)\) is irrational by Chudnovsky's theorem [C1976].
theorem c7b_lower_bound : 2 ≤ C7b
Category research solved; AMS 11 Number theory, 33 Special functions. Declared in FormalConjectures/OptimizationConstants/7b.lean, line 55.
Constant7b.c7b_lower_bound_improved
Open: stated without proof.
Can the current best lower bound be improved?
theorem c7b_lower_bound_improved : 2 < C7b
Category research open; AMS 11 Number theory, 33 Special functions. Declared in FormalConjectures/OptimizationConstants/7b.lean, line 60.
Constant7b.c7b_upper_bound
Solved: stated here without proof.
The first and current best known upper bound, proved by Bruiltet in [Bru2002]. It follows from an explicit lower bound on \(|\Gamma(1/4) - p/q|\) for rational \(p/q\) of sufficiently large height.
theorem c7b_upper_bound : C7b ≤ 10 ^ 143
Category research solved; AMS 11 Number theory, 33 Special functions. Declared in FormalConjectures/OptimizationConstants/7b.lean, line 66.
Constant7b.c7b_upper_bound_improved
Open: stated without proof.
Can the current best upper bound be improved?
theorem c7b_upper_bound_improved : C7b < 10 ^ 143
Category research open; AMS 11 Number theory, 33 Special functions. Declared in FormalConjectures/OptimizationConstants/7b.lean, line 71.
Sources
TheoremTao's Optimization Constant 14 / Smallest \(n\) for which the value of \(BB(n)\) is undecidable#
References: - Tao's Optimization Constant 14 - [LS1965] Lin, S. and Radó, T., Computer studies of Turing machine problems. J. ACM 12 (1965), 196–212. - [B1983] Brady, A. H., The determination of Radó's noncomputable function \(\Sigma(k)\) for four-state Turing machines. Math. Comp. 40 (1983), 647–665. - [BB2025] Blanchard, J. et al., Determination of the fifth Busy Beaver value (2025). arXiv:2509.12337 - [YS2016] Yedidia, A. and Aaronson, S., A relatively small Turing machine whose behavior is independent of set theory (2016). arXiv:1605.04343 - [O2016] O'Rear, S., metamath-turing-machines (2016). - [W2025] Wade, A. J., turing_machine_explorer (2025). - [G2026] Glazer, E., K230: a 230-state Turing machine for the consistency of ZFC (2026). Announcement - [A2020] Aaronson, S., The Busy Beaver Frontier. ACM SIGACT News 51 (2020), 32–54.
This file defines the smallest \(n\) for which the value of \(BB(n)\) is undecidable. More precisely, it formalizes the least number of states for which ZFC can neither prove nor disprove that a specific Turing machine halts. Its existence and known upper bounds follow from Gödel's second incompleteness theorem.
We do this by modeling a version of first order logic, ZFC and Turing machines within Lean. The implementation of FOL and ZFC is taken from the FormalizedLogicLean project. The implementation is copied and minimized from that project. It is not necessary to read it to understand the definition of
C14. The copied definitions span the sectionFormalizedFormalLogic. Confidence in that implementation partly comes from the large body of proofs developed with it, including formalizations of independence theorems.This is followed by a model of Turing machines within the first-order logic framework, developed for Formal Conjectures in the section
BackgroundDefs. The file then definesC14and states its known bounds and related conjectures. The known bounds usesorry; formalizing one would be a substantial achievement.
Quoted from FormalConjectures/OptimizationConstants/14.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The file states 10 research or textbook statements: 3 open and 7 solved.
Constant14.c14_ge_4
Solved: stated here without proof.
Proven by Lin and Radó in [LS1965] by computing \(BB(3) = 21\).
theorem c14_ge_4 : 4 ≤ C14
Category research solved; AMS 03 Mathematical logic and foundations, 68 Computer science. Declared in FormalConjectures/OptimizationConstants/14.lean, line 1729.
Constant14.c14_ge_5
Solved: stated here without proof.
An intermediate lower bound, proved by Brady in [B1983] by explicitly computing \(BB(4) = 107\).
theorem c14_ge_5 : 5 ≤ C14
Category research solved; AMS 03 Mathematical logic and foundations, 68 Computer science. Declared in FormalConjectures/OptimizationConstants/14.lean, line 1734.
Constant14.c14_lower_bound
Solved: stated here without proof.
The current best known lower bound, proved by Blanchard et al. in [BB2025] by explcitily computing \(BB(5) = 47176870\).
Note \(BB(5) = 47176870\) (as well as the values below) has been formally proven in Rocq as part of [BB2025], a formal proof of the declaration below would likely be much more difficult on a technical level than the proof in Rocq, which is based on dependent type theory.
theorem c14_lower_bound : 6 ≤ C14
Category research solved; AMS 03 Mathematical logic and foundations, 68 Computer science. Declared in FormalConjectures/OptimizationConstants/14.lean, line 1743.
Constant14.c14_lower_bound_improved
Open: stated without proof.
Can the current best lower bound be improved?
theorem c14_lower_bound_improved : 6 < C14
Category research open; AMS 03 Mathematical logic and foundations, 68 Computer science. Declared in FormalConjectures/OptimizationConstants/14.lean, line 1747.
Constant14.c14_le_7910
Solved: stated here without proof.
The first known upper bound, proved by Yedidia and Aaronson in [YS2016]. Their construction reduces the independence problem to a graph-theoretic setting.
theorem c14_le_7910 : C14 ≤ 7910
Category research solved; AMS 03 Mathematical logic and foundations, 68 Computer science. Declared in FormalConjectures/OptimizationConstants/14.lean, line 1752.
Constant14.c14_le_748
Solved: stated here without proof.
An intermediate upper bound, proved by O'Rear in [O2016]. It uses a Turing machine that enumerates proofs in ZF.
theorem c14_le_748 : C14 ≤ 748
Category research solved; AMS 03 Mathematical logic and foundations, 68 Computer science. Declared in FormalConjectures/OptimizationConstants/14.lean, line 1757.
Constant14.c14_le_432
Solved: stated here without proof.
An intermediate upper bound, proved by Wade in [W2025]. It refines the proof-enumerating machine construction from [O2016].
theorem c14_le_432 : C14 ≤ 432
Category research solved; AMS 03 Mathematical logic and foundations, 68 Computer science. Declared in FormalConjectures/OptimizationConstants/14.lean, line 1762.
Constant14.c14_upper_bound
Solved: stated here without proof.
The current best known upper bound, from [G2026]. Glazer proved in Rocq, without axioms, that a certain 230-state Turing machine halts if and only if ZFC is inconsistent.
theorem c14_upper_bound : C14 ≤ 230
Category research solved; AMS 03 Mathematical logic and foundations, 68 Computer science. Declared in FormalConjectures/OptimizationConstants/14.lean, line 1767.
Constant14.c14_upper_bound_improved
Open: stated without proof.
Can the current best upper bound be improved?
theorem c14_upper_bound_improved : C14 < 230
Category research open; AMS 03 Mathematical logic and foundations, 68 Computer science. Declared in FormalConjectures/OptimizationConstants/14.lean, line 1771.
Constant14.c14_le_20
Open: stated without proof.
Conjecture 11 in [A2020] by Scott Aaronson
theorem c14_le_20 : C14 ≤ 20
Category research open; AMS 03 Mathematical logic and foundations, 68 Computer science. Declared in FormalConjectures/OptimizationConstants/14.lean, line 1775.
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.