James-Hanson/junk-theorems-in-lean
View on GitHub ↗ ★ 114 Lean
A small collection of formally verified junk theorems provable in Lean4 + Mathlib.
3 mentions on Hacker News by 3 people: 1 story, 2 comments · first 2025-12-23 · latest 2026-09-04
20082026
-
…in a way that can’t be fooled. I would be a bit careful asserting that in full generality, given https://github.com/James-Hanson/junk-theorems-in-lean
comment by stratos123 · 2026-09-04 · in Formalizing Fermat's Last Theorem -
…are pretty subtle, and which really might turn up in e.g. a verified systems programming context: https://github.com/James-Hanson/junk-theorems-in-lean/blob/m... (there is a proof of 0=1 at the end - it is easy to understand where it comes…
comment by Diogenesian · 2026-06-27 · in AI in mathematics is forcing big questions