Summary
The Lean formalization of putnam_1974_b1 appears to remain false in the official PutnamBench source, despite the historical fix that changed the regular-pentagon answer predicate to require B > 0.
The adjacent official answer comment is:
fun p ↦ ∃ᵉ (B > 0) (o : Equiv.Perm (Fin 5)),
∀ i, dist (p (o i)) (p (o (i + 1))) = B
Observed issue
The predicate appears to permit repeated non-adjacent points. A concrete unit-circle configuration of the shape [A, B, C, A, B], where A, B, and C are vertices of an equilateral triangle on the unit circle, satisfies all five cyclic equal-distance constraints with the positive value B = √3. However, its pairwise-distance sum is strictly below that of another valid unit-circle configuration.
Reproduction
To reduce contamination, please contact me for a complete Lean 4.27 counterexample file if needed.
Summary
The Lean formalization of
putnam_1974_b1appears to remain false in the official PutnamBench source, despite the historical fix that changed the regular-pentagon answer predicate to requireB > 0.The adjacent official answer comment is:
Observed issue
The predicate appears to permit repeated non-adjacent points. A concrete unit-circle configuration of the shape
[A, B, C, A, B], whereA,B, andCare vertices of an equilateral triangle on the unit circle, satisfies all five cyclic equal-distance constraints with the positive valueB = √3. However, its pairwise-distance sum is strictly below that of another valid unit-circle configuration.Reproduction
To reduce contamination, please contact me for a complete Lean 4.27 counterexample file if needed.