Lean 4 formalization of constructions and conditional reductions (Erdős-problem context)

Statement

Lean 4 formalization, in the Erdős-problem context, is the practice of re-expressing (a) a mathematical statement (a conjecture, a known theorem, or an explicit combinatorial construction) and, separately and much more expensively, (b) its proof, as a type-checked term in the Lean 4 dependent-type-theory kernel using the mathlib library, so that correctness becomes a mechanical, zero-trust check (the kernel either accepts the term or it doesn't) rather than a matter of human refereeing. Two formalization *targets* recur constantly in this literature and are the specific subject of this page:

1. Formalizing a construction = proving an *existence* statement with an *explicit witness* — e.g. "for every prime power $q$, there is a Sidon set of size $q+1$ modulo $q^2+q+1$" (Singer's construction) — by literally building the Lean term (the finite field $\mathbb F_q$, the degree-3 extension, the trace map, the witness set) and having the kernel check it satisfies the stated property. This is qualitatively different from formalizing an asymptotic *impossibility*/upper-bound proof: a construction's correctness is (in principle) *decidable/checkable pointwise*, so Lean's role is to certify that the general recipe, not just finitely many instances, is bug-free. 2. Formalizing a conditional reduction = proving, as a fully machine-checked, sorry-free implication, a statement of the shape $$H_1 \wedge H_2 \wedge \cdots \wedge H_k \;\Longrightarrow\; C,$$ where $C$ is the target open conjecture and $H_1,\dots,H_k$ are (possibly themselves still-open, but logically weaker or more standard) hypotheses — without resolving the $H_i$ or $C$. The reduction itself becomes a permanent, checkable mathematical fact, decoupled from whether anyone has yet proved the premises. Canonical instance: arXiv:2605.03274 formalizes, in addition to Singer's construction, the fully proved (zero sorry) implication *"subpolynomial prime gaps $\wedge$ a full subpolynomial upper-error hypothesis for the Sidon function $h(N)$ $\Rightarrow$ $h(N)=N^{1/2}+O_\epsilon(N^\epsilon)$ for every $\epsilon>0$"* — i.e. a formal, checked map of exactly what extra input would suffice to resolve Erdős #30 (Erdős #30 — sharp $N^{1/2}$ asymptotics for Sidon sets), even though neither hypothesis is currently known and #30 itself remains open.

Facts

- Scale of the ecosystem (Xena Project blog, Kevin Buzzard, xenaproject.wordpress.com/2025/12/05, and this wiki's own cross-checks): erdosproblems.com (Thomas Bloom, since May 2023) catalogues 1100+ Erdős problems, ~40% marked solved; roughly **~240 problems have a formalized Lean *statement* and only ~17 have a fully formalized *proof/solution* — the statement-vs-solution gap is large and is the main bottleneck this whole line of work is chipping at. - google-deepmind/formal-conjectures (launched May 2025) is the primary statement bank: "a collection of formalised statements of conjectures in Lean, using mathlib," explicitly scoped to statement-only** formalization (proofs deliberately sorry'd for the open cases) so it can double as an automated-theorem-prover benchmark and as a mathlib-gap detector. Conventions used throughout (confirmed directly from the repo and from this wiki's own per-problem .lean-file reads): each theorem carries @[category research open] / @[category research solved] tags (the *tag* reflects informal literature status, independent of whether the Lean *proof* itself is filled in — a solved-in-the-literature result can still be sorry'd in Lean, and often is); the target value of an unknown quantity is wrapped in an answer(sorry) elaborator when no closed form is even conjectured (e.g. erdos_40, erdos_138 in this wiki's own verified reads); named sub-theorems (e.g. erdos_40.variants.implies_erdos_28, erdos_123.variants.powers_2_3_5_snug) record specific special cases, implications, or strengthenings as separate, individually-sorry-trackable Lean declarations. - Concrete worked example — Singer construction + conditional reduction (Erdős #30): Hulak, Ramos, de Queiroz, "Formalizing Singer Sidon Constructions and Sidon Set Infrastructure in Lean 4," arXiv:2605.03274 (May 2026). 7,541 lines of Lean 4, zero active `sorry`. Formalizes (i) Singer's finite-field/projective-plane construction as an existence theorem with an explicit witness (base field → degree-3 extension → trace-kernel 2-dim subspace → geometric subspace-intersection argument for the multiplicative Sidon property → transfer to additive integers mod $q^2+q+1$), and (ii) the conditional reduction described in Statement above. The paper's own framing: mechanization "clarifies the precise scope of classical arguments and forces explicit treatment of the passage from the field-theoretic construction to integer Sidon predicates" — i.e. formalizing a construction routinely surfaces implicit steps (projective-vs-affine representatives, modular-to-interval transfer, degenerate small-$q$ cases) that informal papers gloss over. - Named AI-formalization precedents already tracked in this wiki, each independently source-verified: - erdos/1014 (Ramsey increment problem): "solved by an internal model at OpenAI," proof status PROVED (LEAN) on erdosproblems.com. - Erdős #138 — does W(k)^{1/k} → ∞ for van der Waerden numbers? ($500 van der Waerden question): the "difference" sub-variant $W(k+1)\ge W(k)+k$ was proved by a DeepMind prover agent inside formal-conjectures, then generalized informally by Adam Zsolt Wagner, Thomas Bloom, and Nat Sothanaphan (using GPT-5.4) in the erdosproblems.com forum thread — an example of Lean-verified AI output seeding further *human/LLM-hybrid* informal progress on stronger variants. - Erdős #165 — asymptotic formula for the Ramsey number R(3,k) (Ramsey $R(3,k)$ constant): the record-holding papers (Hefty–Horn–King–Pfender arXiv:2510.19718 and Bradač arXiv:2605.28793) were autoformalized end-to-end, after the fact, by the Trellis system (math.cmu.edu/~wes/trellis.php, an LLM-agent — ChatGPT Pro/Codex — autoformalizer with a deterministic supervisor and human oversight only on Lean "shape" approval); the Bradač formalization took ~40 hours wall-clock and ~$18 of compute. - Erdős #39 — density $N^{1/2-\\epsilon}$ infinite Sidon set/family (Sidon sets): Alexeev & Mixon, "Forbidden Sidon subsets of perfect difference sets, featuring a human-assisted proof," arXiv:2510.19804 (Oct 2025, rev. Jan 2026, publ. PNAS 2026) — resolves a separate $1000 Erdős prize (not every finite Sidon set extends to a perfect difference set; counterexample $\{1,2,4,8,13\}$) with correctness of the counterexample checked via a ChatGPT-"vibe-coded" Lean 4 proof, ancillary files on arXiv, fully reproducible. - Boris Alexeev's plby/lean-proofs repo runs an explicit ChatGPT → Aristotle pipeline (per the Xena blog post): ChatGPT produces/explains an informal solution, Aristotle auto-formalizes it into Lean, with automatic posting back to GitHub once compiled; later stages of the same pipeline became "fully autonomous" (Aristotle/AlphaProof solving and formalizing without a human-supplied informal proof at all). - Failure modes, documented directly (Xena blog post, first-person account of misformalizing statements): three recurring bug categories were found — (1) low-level bugs (flipped inequalities, wrong variable bound), (2) missing hypotheses, (3) high-level conceptual misunderstandings of what the informal statement meant — several caught only when an AI formalization/search tool found a trivial counterexample exploiting the oversight (e.g. unhandled "junk values" from division by zero). This is a direct, source-confirmed illustration of why formalizing constructions is valuable even when the underlying math is "already known": Lean forces every edge case to be discharged explicitly. - Broader autoformalization tooling referenced in the same literature search: "Lean Atlas" (arXiv:2604.16347, human-AI collaborative formalization environment) and "LeanMarathon" (arXiv:2606.05400, long-horizon autoformalization; reports 7 target theorems across 4 Erdős problems — #1051, #1196, #164, #1217 — formalized with no sorry, including a formalized proof of the Erdős–Graham irrationality problem #1051) — both existence/scope only confirmed via WebSearch snippets, not independently fetched in full in this session.

Technique

When it applies: - Best-suited target #1 — explicit, checkable constructions: finite or algorithmically-generated combinatorial objects (Sidon/difference sets via finite fields, Danzer/Fishburn–Reeds equidistant-point configurations with exact algebraic coordinates, Golomb rulers, small-case counterexamples) where the defining property (distinctness of sums, convex position, coincidence of distances) is *decidable in exact arithmetic*. Lean+mathlib is a near-ideal fit because the witness itself is finite/algorithmic and the "does it work" check is exactly what a kernel typechecker is built to do. - Best-suited target #2 — logical reductions between statements, especially ones already informally known or suspected in the literature ("if X (a standard-looking but still-open hypothesis) then Y (the target conjecture)"), where the *interesting content* is the implication's correctness, not the truth of $X$. Formalizing this severs the reduction from the fate of the open hypotheses — it becomes permanent derivation scaffolding usable by anyone who later proves (or imports from elsewhere) $H_1,\dots,H_k$. - Not (yet, per every example found) a primary tool for *discovering* new asymptotic/analytic results on genuinely open conjectures: in every source checked in this wiki (erdos/30, /89, /97, /107, /123, /138, /165), the pattern is that Lean formalization runs *behind* the mathematics — either formalizing an already-published proof (Guth–Katz, Berlekamp/Gowers bounds, HHKP25/Bradač), or formalizing the *statement* of the open conjecture itself while leaving sorry on the hard direction. The one clean counterexample to "always behind" is the conditional-reduction pattern (arXiv:2605.03274), where the *reduction itself* is new mathematics produced *through* the formalization process, not merely transcribed into it.

Why it works (the mechanism): - A conditional reduction $H_1\wedge\cdots\wedge H_k\Rightarrow C$ is, in Lean's dependent type theory, simply a function/term of the corresponding Pi-type/implication type. Producing a sorry-free term of that type is a fully mechanical, zero-trust proof that the implication holds *as stated* — independent of whether $H_1,\dots,H_k$ or $C$ have truth values known to anyone. This is exactly what lets a formalization be useful before the surrounding open problem is resolved: it pins down, unambiguously and machine-checked, the *exact logical gap* remaining (arXiv:2605.03274's contribution to Erdős #30 is precisely this — "prime gaps subpolynomial + a subpolynomial $h(N)$ upper-error bound suffice," nothing more, nothing less, no informal fudge factor). - For constructions, the mechanism is that Lean forces every step to actually typecheck, including the steps an informal paper elides (projective-vs-affine coordinate choices, small-parameter degenerate cases, the modular-to-integer-interval transfer for Singer's construction). Because the kernel accepts *no* implicit reasoning, formalizing a construction is a strong, automatic audit: bugs that survive human refereeing (wrong inequality direction, an unhandled edge case, a sorry-shaped hole papered over informally) get caught the moment the term fails to typecheck — precisely the failure modes catalogued in the Xena blog post. - The ecosystem structure (statement bank formal-conjectures maintained separately from proof repos like plby/lean-proofs, Trellis, Lean Atlas) exists because formalizing a *statement* correctly is itself nontrivial and valuable in isolation (it clarifies ambiguous natural-language conjectures, and gives autoformalizer/ATP systems and human contributors alike a stable, unambiguous target) — this is why erdosproblems.com tracks "formalized statement" and "formalized solution" as two separate, independently-reported axes of progress, and why the wiki's own problem pages consistently distinguish "the conjecture is stated but sorry'd" from "a machine-checked proof exists."

How to actually use it (recipe, as instantiated across the examples above): 1. Pick a target: either (a) an explicit construction whose defining property is exact-arithmetic-checkable, or (b) a plausible-looking conditional reduction of an open conjecture to more tractable/standard hypotheses (often visible informally in a survey or in the problem's own literature — e.g. "this would follow from $X$" remarks). 2. State it precisely in Lean 4 + mathlib, ideally against (or contributing to) google-deepmind/formal-conjectures's existing statement conventions (@[category ...], answer(sorry) for unknown target values) so it's discoverable and mergeable into the shared statement bank. 3. Fill the proof: for constructions, build the explicit witness term (field extensions, trace maps, coordinate representatives) and let the kernel force every implicit case split into the open; for reductions, chain existing mathlib lemmas (or newly-proved auxiliary lemmas) into the implication, using the informal literature's proof sketch as a guide but resolving every gap the informal version left implicit. 4. Optionally automate steps 2–3 with an LLM pipeline (ChatGPT/GPT-5.x for the informal sketch → Aristotle/AlphaProof/Trellis/Codex-agent for the Lean tactic proof), with the Lean kernel itself as the final, fully mechanical verifier — this is the workflow explicitly documented for plby/lean-proofs and Trellis, and is what let a handful of AI-touched formalizations (erdos/1014, the Bradač off-diagonal Ramsey paper, the Alexeev–Mixon Sidon counterexample) go from informal claim to sorry-free Lean in hours-to-days rather than the months a fully manual formalization historically took (the original erdosproblems.com hand-formalization pass took Jan–Jul 2022, six months, per the Xena blog post). 5. Report status back into the tracked ecosystem (erdosproblems.com's "Formalised statement/solution" fields, formal-conjectures's category tags) so the sorry-vs-proved distinction stays an accurate, checkable public record rather than an informal claim.

Related

- Erdős #30 — sharp $N^{1/2}$ asymptotics for Sidon sets — the canonical worked example: Singer's Sidon construction formalized with zero sorry plus the fully machine-checked conditional reduction (prime gaps subpolynomial + subpolynomial upper-error hypothesis $\Rightarrow$ the Erdős #30 estimate), arXiv:2605.03274. - Singer finite-field perfect difference set construction — the mathematical content of the construction being formalized in arXiv:2605.03274; this page is the formalization-technique companion. - Sidon sets / B_2 sets / Golomb rulers — the broader combinatorial-object family whose extremal-function literature (erdos/30, /39, /40, /241, /840, /845) is the single densest cluster of Lean-formalization activity found in this wiki. - Erdős #1 — distinct subset sums need N ≫ 2^n — statement formalized (google-deepmind/formal-conjectures), only the trivial weaker bound proved in Lean; concrete unclaimed formalization target. - Erdős #40 — sharp density threshold for Erdős–Turán — statement formalized including a fully-proved implication sub-variant (erdos_40.variants.implies_erdos_28), main question answer(sorry); a second worked example of the conditional-reduction-between-two-open-problems pattern, alongside erdos/30's arXiv:2605.03274. - Erdős #138 — does W(k)^{1/k} → ∞ for van der Waerden numbers? — the difference-variant of the $500 van der Waerden question, proved by a DeepMind prover agent directly inside formal-conjectures, then generalized informally in the forum — an example of Lean-verified output seeding further human/LLM progress. - Erdős #165 — asymptotic formula for the Ramsey number R(3,k) — Ramsey $R(3,k)$; record papers (HHKP25, Bradač) autoformalized post-hoc by the Trellis LLM-agent system at ~$18 compute for the harder one, a concrete cost/time data point for this whole technique. - erdos/1014 — adjacent Ramsey-increment problem, "solved by an internal model at OpenAI," status PROVED (LEAN) on erdosproblems.com — the clearest example in this wiki of an AI system producing new, Lean-verified mathematics rather than formalizing a pre-existing human proof. - Erdős #97 — convex polygon vertex with no 4 equidistant and Erdős #89 — distinct distances in the plane — both have Lean *statements* (including already-published sub-results like Guth–Katz and the Danzer/Fishburn–Reeds constructions) entirely sorry'd, illustrating that "formalized" on erdosproblems.com must not be read as "verified" — concrete, low-risk, currently-unclaimed formalization targets independent of resolving the open conjecture itself.