[aznikline]

Summary

Registers a sorry-free partial Lean 4 formalization of Sendov's solution of Blumenthal's minimax-angle problem (Erdős problem 504), pointing to a pinned commit in a public repository owned by the submitting account (aznikline). The Lean proof field remains No — this is a partial artifact, submitted for the record and for maintainer review, following the precedent format of #5080.

What the pinned artifact proves

All results below are kernel-checked; every #print axioms audit reports exactly [propext, Classical.choice, Quot.sound] — no sorry, no admit, no native_decide, no custom axioms anywhere in the repository.

• Jsp404.sendov_upper — sharpness for all N ≥ 3: explicit extremal configurations whose largest angle is ≤ alphaN N + ε (vendored, attributed constructions + proofs).
• Jsp404.sendov_lower_le_eight / Jsp404.sendov_alpha_eq_le_eight — the exact value α(N) = alphaN N for 3 ≤ N ≤ 8, unconditional.
• Jsp404.sendov_alpha_eq_of_geometricCertificates — the complete Sendov classification JSP404.alpha N = alphaN N for all N ≥ 3, conditional on GeometricCertificates.
• Jsp404.sendov_lower — the PtCfg-form lower bound for all N ≥ 3, conditional on the same hypothesis.

The remaining gap, stated exactly

GeometricCertificates (defined in Jsp000404/CertificateIntegration.lean) is the strip-wise existence claim CertExists for strips n ≥ 3 — the weighted-capacity/dichotomy step that Sendov's paper performs by a brief sketch. The n = 1 and n = 2 strips are discharged unconditionally; N ≤ 8 needs no certificate. The unconditional N ≥ 9 lower bound is the single missing piece. The hypothesis is an ordinary Lean proposition taken as a parameter — not an axiom.

Several plausible helper lemmas (maxGap_boundary_emission, unrestricted staircase bounds, unrestricted removable-vertex existence) were found false as naively quantified during the campaign — kernel-checked countermodels were constructed — and are therefore deliberately absent from the artifact rather than stated with sorry.

Statement origin / correspondence

The catalog asks for the largest angle every planar N-point set must determine — Sendov's alphaN (Acta Math. Hungar. 69 (1995), Theorem 4.1). The artifact proves the classification exactly for N ≤ 8, sharpness for all N, and reduces the general case to one explicitly named hypothesis. Note: erdosproblems.com/504's displayed formula has a typo in the first branch (numerator 1 vs 2); alphaN in the artifact follows the published theorem (verified against N = 5).

Lean formalization repository

• Repository: https://github.com/aznikline/jsp-000404-lean
• Pinned commit: cbfbbef188f5f98eead6045d7c3548de3c1b701a (branch master)
• Key theorems: Jsp404.sendov_upper, Jsp404.sendov_alpha_eq_le_eight, Jsp404.sendov_alpha_eq_of_geometricCertificates, Jsp404.sendov_lower
• Toolchain: Lean leanprover/lean4:v4.34.0, Mathlib 5ed2965256430c3649e86755f9576b54eca72435 (lean-toolchain, lake-manifest.json)

Reproduction

git clone https://github.com/aznikline/jsp-000404-lean && cd jsp-000404-lean
git checkout cbfbbef188f5f98eead6045d7c3548de3c1b701a
lake exe cache get && lake build

Compiles cleanly from a fresh clone at the pinned commit (3293 jobs, zero sorry warnings). Axiom audit instructions are in the repository README.md.

Attribution

Formalization contributor: aznikline. The repository vendors, unmodified and with attribution retained (ThirdParty/Sendov/, MIT + CC BY 4.0 docs), the sharpness constructions of superpilot69/awards@722cb3ca (superpilot69 and ChatGPT 6 Astra).

Checklist

• Lean proof remains No — partial scope stated explicitly
• Lean source is public and pinned to an immutable commit
• No sorry/admit/native_decide/custom axioms (verified by build + #print axioms)
• Reproduction commands verified on a clean build
• Third-party vendored code carries retained license and attribution

[Federico2014]

Thank you for your submission. Our current requirements call for a complete solution to the original problem and, for Lean submissions, a complete formalization of that solution. Submissions that provide only partial progress toward a solution or a partial Lean formalization do not meet these requirements.

We are therefore closing this PR. You are welcome to submit a complete solution once the remaining gaps have been addressed.