A single catalogue of active and completed projects. Status labels describe mathematical and verification maturity; linked repositories contain the technical record.
2026
Greedy Uniformity on Trees: Exact Obstruction and Near-Uniform Spiders
arXiv preprint
Random-order greedy maximal independent sets are exactly uniform on a finite tree only for K₁ and K₂, while explicit spiders approach uniformity.
For a uniformly random ordering of the vertices of a finite tree, this project compares the greedy maximal-independent-set law with the uniform law on maximal independent sets. It proves exact uniformity iff the tree is K₁ or K₂, and gives an explicit mixed-spider family Tk,2k−k with positive total-variation bias O(k/4k)=O(lognk/nk2) along nk=2k+k+1. The frozen A+B package is formalised in Lean and registered with Palomar; the all-n extremal minimisation problem and optimality of the construction remain open. The literature audit supports only “plausibly new with bounded uncertainty”, not an unconditional historical-priority claim.
Combinatorics
Graph theory
Probability
Greedy algorithms
Maximal independent sets
Trees
Lean 4
Mathlib
Date
2026-10-05
Formalisation
Lean 4.35.0-rc3 / Mathlib v4.35.0-rc3
Verification
Lean 4.35.0-rc3 / Mathlib commit c55e6e786f49471c72fbddbec5415808896aec1e machine-checks the exact finite-law bridge, both final Theorem A declarations and all seven final Theorem B checkpoints; axiom checks report only propext, Classical.choice and Quot.sound, with no project-specific axioms or sorry/admit/native_decide in the project Lean sources. GitHub Actions passed the complete Lean build and 5 Python regression tests, while exact computation checks all 436 nonisomorphic unlabeled trees on 1–11 vertices and targeted local proof certificates. Palomar entry PALOMAR-2026-10-01-000003, version 1, is registered with high trust from immutable source commit 1733c29a5165148d71a2f0bd1ed2dcd7c35309ce. Lean and Palomar verify the formal statements and package integrity; they are not peer review or novelty certification.
Palomar
PALOMAR-2026-10-01-000003
arXiv
2610.02276
DOI
10.48550/arXiv.2610.02276
Attribution: John Fairfax-Ball is the author and repository maintainer. The random-order greedy maximal-independent-set / iid-priority / random-sequential-adsorption process is established prior art; Gadouleau–Kutner already exhibit the unequal P₃ permutation fibres, and Sagan–Vatter provide standard maximal-independent-set counting machinery used as background. This project’s audited contribution is the exact finite-tree obstruction and the explicit near-uniform mixed-spider family; Mathlib supplies foundational library results and Palomar supplies an external registry/verification record. The literature search supports only “plausibly new with bounded uncertainty”.
Prior / source research: John Fairfax-Ball, “Greedy Uniformity on Trees: Exact Obstruction and Near-Uniform Spiders”, arXiv:2610.02276 (2026). Relevant prior context includes Michael Krivelevich, Tamás Mészáros, Peleg Michaeli and Clara Shikhelman, “Greedy maximal independent sets via local limits”, arXiv:1907.07216 / Random Structures & Algorithms; Ivan Kryven, Rik Versendaal and Mike de Vries, “Unified framework for asymptotically uniform iterative construction of generalised random graphs with local constraints”, arXiv:2608.07239v1 (2026); and Maximilien Gadouleau and David C. Kutner, “Generalising the maximum independent set algorithm via Boolean networks”, Information and Computation 303 (2025), 105266.
Sharp p-adic extrema and least extremal rows for restricted binomial GCDs are Lean-verified and public as arXiv:2610.01328.
This project studies sharp p-adic valuations of restricted binomial GCDs G(N;m), where lower indices are multiples of m. It proves that for every prime p with p∤m the maximum valuation over admissible rows is exactly r_p(m), constructs an attaining row, and for m=p^a+1 with a≥2 proves the exact least extremal row Tp(pa+1)=p3a+1; no general closed formula for T_p(m) is claimed. All stated target theorems are formally verified in Lean, with finite experiments retained only as independent checks. A documented literature audit located no equivalent theorem for the remaining general results beyond attributed prior subcases, but this is a negative-search finding and theorem-level non-overlap with Chung–Yang (2026) remains unresolved because its full text was not openly inspectable.
Number theory
Binomial coefficients
Greatest common divisors
p-adic valuations
Extremal problems
Lean 4
Mathlib
Date
2026-10-01
Formalisation
Lean 4 / Mathlib
Verification
Lean 4 / Mathlib formalises Target A's universal upper bound, constructive attainment and exact maximum, establishes existence and minimality of the least extremal row T, and formalises Target B's target-row valuation plus strict lower-row non-attainment, yielding T p (p^a+1) = p^(3a)+1 for every prime p and a≥2. Repository CI builds the project from a fresh checkout and rejects sorry/admit in project Lean sources. Palomar entry PALOMAR-2026-09-30-000033, version 1, registered the advertised Target-A/Target-B theorem surface after successful Comparator and kernel verification. The Stage-2 seven-case pilot was independently checked by a Kummer carry/borrow DP against direct Legendre and integer binomial/GCD implementations; those computations are finite evidence only and remain outside the proof and formal trust boundary.
Palomar
PALOMAR-2026-09-30-000033
arXiv
2610.01328
Attribution: John Fairfax-Ball is the author of the project, paper and Lean formalisation. Chai Wah Wu's 2026 work defines the exact selected-binomial-GCD family, while Carl McTague's work contains the p≡1 (mod m) Target-A subcase and the known (p,m,N)=(2,3,6) case; Kummer's theorem and Mathlib's p-adic/digit infrastructure are prior tools. Compatible low-level Lean infrastructure was adapted with attribution from the Apache-2.0 Pascal Minus-One predecessor. The documented September 2026 literature audit located no equivalent result for the remaining general Target-A theorem or Target B, subject to the unresolved Chung–Yang 2026 full-text caveat; this is not an unconditional historical-priority claim.
Prior / source research: Research continuation of John Fairfax-Ball's Pascal Minus-One GCD project (2026). Core prior mathematical context: Chai Wah Wu, “Computing the Greatest Common Divisor of Binomial Coefficients C(mn,mk)”, arXiv:2606.20940v2 (2026), defines exactly the selected-GCD family; Carl McTague, “On the Greatest Common Divisor of Binomial Coefficients C(n,q), C(n,2q), C(n,3q), ...”, American Mathematical Monthly 124(4) (2017), 353–356, corrected arXiv:1510.06696v5, contains the p≡1 (mod m) overlap and the (2,3,6) example.
A proved fixed-offset threshold theorem for random stackability on paths, with key finite deterministic interfaces formalised in Lean 4 and a public arXiv preprint.
ProbStack studies support-collapse stackability for uniformly random weak compositions of pebbles on paths and trees. For paths, the project proves a two-sided fixed-offset threshold centred at log2n−21log2log2n+log2(3e), with no claim at zero offset. The full asymptotic argument remains paper mathematics; Lean 4 formalises the exact finite TreeStack/path interfaces and the P6 deep-message necessity theorem, including the fixed-total −(2μ−1) corollary.
Probabilistic combinatorics
Graph pebbling
Random structures
Threshold phenomena
Trees and paths
Lean 4
Mathlib
Date
2026-09-30
Formalisation
Lean 4 / Mathlib
Verification
The finite P6 necessity theorem and its exact fixed-total corollary are Lean-formalised without project sorry or axiom declarations in the ProbStack proof development and are publicly registered with Palomar as PALOMAR-2026-09-30-000023, version 1. Exhaustive and regression checks support the finite interfaces. The full random asymptotic threshold theorem is not part of the Palomar registration and is not fully Lean-formalised.
Palomar
PALOMAR-2026-09-30-000023
arXiv
2609.39633
DOI
10.48550/arXiv.2609.39633
Attribution: John Fairfax-Ball developed and maintains ProbStack and its Lean formalisation. The project uses TreeStack's deterministic structural stackability certificate as an input; Csernák and Soukup provide the support-collapse stacking context, and Bushaw and Kettle provide closely related random-pebbling path asymptotics for the different solvability event. A substantial 2026 public-record prior-art audit found no exact match in the searched sources for ProbStack's random fixed-total support-collapse stackability theorem on paths. Classical ingredients and the closest related results are explicitly attributed; this is a public-record originality finding rather than an unconditional historical-priority claim.
Prior / source research: TreeStack — Structural Certificates for Stacking on Trees (John Fairfax-Ball), together with the graph-pebbling background cited in formalization.yaml: Tamás Csernák and Lajos Soukup, “Stacking and clearing in graph pebbling” (arXiv:2604.22341), and Neal Bushaw and Nathan Kettle, “Thresholds for pebbling on grids” (arXiv:2309.01762).
Lean/Mathlib formalisation complete, Palomar verified, and the research paper is public as arXiv:2609.37754 [math.NT].
This project studies G(N;m)=gcd{(kN):0<k<N,m∣k}. It formally proves the p≡−1(modm) valuation theorem, the complementary p≡1(modm) branch, a prime-power scaling theorem and complete prime-by-prime valuation corollaries for m=3,4,6. A source-level audit through 25 September 2026 located no equivalent prior theorem for the full minus-one classification; this is a negative-search statement rather than an unconditional historical-priority claim. The research paper is public as arXiv:2609.37754 [math.NT], v1 submitted 29 September 2026.
Number theory
Binomial coefficients
Greatest common divisors
p-adic valuations
Lean 4
Mathlib
Date
2026-09-29
Formalisation
Lean 4 / Mathlib
Verification
Lean-verified theorem layer: minus-one valuation, plus-one valuation, scaling, and complete modulus 3, 4 and 6 valuation corollaries. CI checks the build, regression tests, reference sweep and zero-sorry gate. Palomar registry entry: PALOMAR-2026-09-25-000017, version 1. Research paper: arXiv:2609.37754 [math.NT], v1 submitted 29 September 2026.
Palomar
PALOMAR-2026-09-25-000017
arXiv
2609.37754
Attribution: John Fairfax-Ball maintains the repository and its Lean formalisation. Mathlib supplies Kummer's theorem and supporting digit machinery. McTague's work gives the plus-one theorem and strict subfamilies of the minus-one side; the September 2026 audit located no equivalent prior theorem for the full minus-one classification.
Prior / source research: Carl McTague, “On the Greatest Common Divisor of Binomial Coefficients C(n,q), C(n,2q), C(n,3q), ...”, American Mathematical Monthly 124(4) (2017), 353–356, corrected arXiv:1510.06696v5. Chai Wah Wu, “Computing the Greatest Common Divisor of Binomial Coefficients C(mn,mk)”, arXiv:2606.20940v2 (2026), is also directly relevant.
TreeStack — Structural Certificates for Stacking on Trees
arXiv preprint
A Lean 4 proof of the corrected nontrivial-tree form of the Csernák–Soukup tree-stacking estimator conjecture.
For every finite tree T with at least two vertices, this project proves stack(T)=estim(T), the corrected nontrivial-tree form of the Csernák–Soukup estimator conjecture. The result is machine-checked end to end in Lean 4 and publicly registered after Palomar mechanical verification and automated review. The standalone research article is publicly available as arXiv:2609.31811 [math.CO].
Graph theory
Graph pebbling
Formal verification
Date
2026-09-21
Formalisation
Lean 4
Verification
The Lean 4 formalisation machine-checks the main theorem end to end. Palomar mechanical verification and automated review passed for revision 4d4969703a9f0ca7a51cbe7edf0f0338cc95cafb; the result is publicly registered as PALOMAR-2026-09-25-000010, version 1.
Palomar
PALOMAR-2026-09-25-000010
arXiv
2609.31811
Attribution: Original conjecture and estimator: Tamás Csernák and Lajos Soukup. Proof, Lean 4 formalisation, computational validation and research article: John Fairfax-Ball, with extensive AI assistance documented in the repository.
Prior / source research: Tamás Csernák and Lajos Soukup, “Stacking and clearing in graph pebbling”, arXiv:2604.22341v1, Conjecture 10.3.