solve(ErdosProblems): piepmeyer in 100

[theaustinhatfield]

Proof generated by Gemini 3.1 pro in Aletheia style harness I made for asiprize.com and verified via Lean 4 compilation. The model extracted the exact algebraic Cartesian coordinates for Lothar Piepmeyer's 9-point planar configuration (using the algebraic seed constant $x = (1+\sqrt{2})\sqrt{2-\sqrt{3}}$) and verified the bounds.

This resolves erdos_100_piepmeyer. The file has been verified locally against the repo's toolchain (rc=0) and DistancesSeparated has been fully proven over the 9 points.

All 7 verification layers passed. The proof uses a custom Term Rewriting System mapping the Euclidean distances to a finite set D to prevent ring and norm_num timeouts over the highly nested radicals.

Axioms checked: clean (propext, Classical.choice, Quot.sound).

Attributes changed: Added @[category research solved, AMS 52] and @[category research formally solved using formal_conjectures at "", AMS 52].

[theaustinhatfield]

@mo271 @Paul-Lez

The Build project CI check timed out after 22 minutes.

This proof heavily utilizes nlinarith and ring_nf across a 2,000–line generated Term Rewriting System to verify the explicit Euclidean distances of Piepmeyer's 9–point planar configuration without triggering Lean's nested radical timeouts.

Because of the massive amount of computational reflection, the GitHub Actions runner doesn't have enough juice to compile it within the default limits :( However, the file compiles cleanly (rc=0) with zero warnings or errors locally on a standard 4–vCPU droplet in under 3 minutes, and DistancesSeparated is fully checked.

Could one of you pull the branch locally to verify the build, or bump the CI timeout limit for this run? Let me know if you'd like me to optimize the dsimp calls to speed up the elaborator further. Thank You!

[franzhusch]

Hi Austin,

thanks for your submission. As you already mentioned, the proof led to a timeout in CI. This is part of the reason (the other being maintainability during bumps), why Formal Conjectures only allows small proofs. If you want to submit this result, the intended way is to just change the category "to formally solved at ", you can just host the proof at your fork of formal conjectures for example. Or somewhere else.