Howardism · Vol. 03Plate II · No. 02
Formal Methods, tagged.
Notes2TagFormal MethodsOldest23 May 2026Newest23 May 2026
Every article tagged formal methods, newest first.
| Title | Summary | Date |
|---|---|---|
| AI-Driven Formal Proof Search | LLM generates Lean, compiler verifies every step → eliminates hallucination; DeepMind resolves 9/353 Erdős + 44/492 OEIS open problems; verification as a filter for human review | |
| Lean | Proof assistant whose compiler mechanically verifies every step; the `sorry` placeholder enables proof sketches; mathlib maturity gates the reachable frontier |