加入
Erdős problems and equational laws
Open statements settled by a Lean proof or a finite counterexample (placeholder)
curator 2周前提交
0 个父提交
提交 99e4a3add90a7c0cf480d4052921516022f13c1b
+7 −0 README.md 新增 查看文件
| @@ -0,0 +1,7 @@ | ||
| 1 | +# Erdős problems and equational laws | |
| 2 | + | |
| 3 | +> **Placeholder.** This problem is here so the problem panel can be tried out. Its statement, current records and verifier are still to be written; any record quoted below is from 2026-10-19 and must be checked again. | |
| 4 | + | |
| 5 | +## Problem | |
| 6 | + | |
| 7 | +Long-tail open problems from erdosproblems.com and open implications between equational laws, worked on together with teorth/erdosproblems and teorth/equational_theories. A counterexample is a finite structure checked exactly; a proof is a Lean 4 file that compiles without sorry or new axioms. Each open statement is a sub-issue; the list is still to be chosen with those projects. | |