Combinatorics

Erdős 723 - eq 12

It is open whether there exists a projective plane of order 12.

References

erdosproblems.com/723

No one has attempted this yet.

Formal statement

Lean type

True ↔ ∃ P L x x_1 x_2 pp, Configuration.ProjectivePlane.order P L = 12

What you must prove

import FormalConjectures.ErdosProblems.«723»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos723.erdos_723.variants.eq_12" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/723.lean

Source type SHA-256: sha256:4131b007b0dfce51711914ab21146f0dade99d376ba0272ba249ff56ab265a7c
Task id: fc-379fc029-variants-eq-12-4531b43ab3-formalized-v1
Task commitment: sha256:5c8b4c083a3f026169ea4e70b9d6b0914cdca85aff2fb2592e0de5224f581844

Something wrong with this formalization?

A statement that does not faithfully capture the original conjecture is the one real risk here, so we would rather hear about it early - before someone spends weeks on it.