Record Lean solution for Erdős Problem 593

[SamPetkov]

Summary

Records a Lean formalization of the finite classification in Erdős Problem 593 while leaving the human-reviewed informal_status as open.

The linked artifact is the deterministic one-file source closure at an immutable commit:

• Erdos593SelfContained.lean

Its final public endpoints are:

• Erdos593.TripleSystem.isObligatory_iff_isolatedReduction_intrinsic
• Erdos593.TripleSystem.isObligatory_iff_constructible_isolatedReduction

Validation

At the linked commit:

• the deterministic standalone-generation check passed;
• the complete standalone file compiled with -DwarningAsError=true;
• the focused Lean wrapper builds and strict source checks passed;
• the project records no sorry, admit, project axiom, unsafe, or sorryAx in the source closure, and the final endpoints use only standard Lean axioms.

Upstream evidence: Lean focused checks.

For this database change, python scripts/validate.py reports Validation OK; it notes that the derived status will become open (Lean).

Provenance and AI disclosure

Eric Li's arXiv:2606.24882 is credited in the formalization repository as the first publicly posted complete proof and as the source of the shared high-level architecture. The Lean implementation was developed with substantial AI-assisted proof and coding tools, followed by Lean kernel replay, source-hygiene checks, and axiom auditing. This PR claims a machine-checked implementation, not independent mathematical priority or external peer review.