AI Proof WatchKeep up with AI contributions

AI-derived bounds for Mazur’s greedy drawing construction

For a well-formed Mazur edge, cycle, series and join scheme with n≥2 vertices and j nontrivial joins, the span satisfies T+1≤2^j(n−2j), with equality at (n,j)=(2,0) or 2j+3≤n. Its worst case is T=2^(n/2)−1 for even n and T=3·2^((n−3)/2)−1 for odd n. Companion theorems give interior dart mass ≤aₛbₛT, Dirichlet row norm ≤2(n−1)²T and |det M|≤(2(n−1)²T)^n, bound the candidate products T²|det M| and T³|det M|, and prove z=adj(M)u with Mz=Δu and boundary zₛ=Δhₛ(T−hₛ) when hₛ≤T, where Δ=det M.

Sources for this record

What was already known

Mazur supplied the integer-height recurrence and Dirichlet weights for a convex greedy drawing. He did not give these quantitative span or product bounds.

AI involvement AI-led

JD Jones directed the project. Grok 4.6 derived the quantitative bounds and Lean proofs from Mazur’s human-authored recurrence and drawing construction. Jones set scope and checked the statements against Mazur; a completed human proof check is not documented.

Grok selected and derived the new quantitative claims and wrote their proofs under Jones's scope direction, using Mazur's human-authored construction as the baseline.

Importance Modest

Quantifies the height growth and related algebraic quantities of an existing construction.

Limitations

The exponential bounds apply to the stated scheme grammar. They do not prove that every graph attains its maximum, a drawing grid bound, a nonzero determinant, or Mazur’s drawing-existence theorem.

Technical verification Formal (Lean 4/Mathlib kernel, Comparator and NanoDa)

Palomar reports Comparator matching of fifteen exact declarations, Lean kernel checking and independent NanoDa replay for the cited commit. This checks the grammar-span and other stated formulas, including their hypotheses; it does not verify a polynomial grid theorem, nonzero determinant or Mazur's separate drawing existence claim. The batch review did not rerun the checker.

Formal checking

statement/definition comparison, kernel proof check and independent exported-proof replay with standard permitted axioms

Checker
Palomar Comparator, Lean kernel and NanoDa
Scope
The fifteen checked Mazur-span statements: exact scheme span, dart-mass and Dirichlet bounds, product-size formulas and adjugate identity.
Basis
Reported by the linked checker
Evidence source

Checking a formal statement does not establish that it matches the original problem.

Human understanding Few

The repository provides a readable derivation, but attributes the mathematical derivation and documentation to Grok and records no named human explanation of the central extremal argument. Few is the missing-evidence default, not a finding that Jones or Mazur cannot understand it.

Correction and publication history

2026-10-18 · publication

Quantifies the height growth and related algebraic quantities of an existing construction.

Read this published revision