Non-trivial error in physics paper found via Lean
leanexplorer
21 points
2 comments
March 22, 2026
Related Discussions
Found 5 related stories in 45.1ms across 3,471 title embeddings via pgvector HNSW
- The case for zero-error horizons in trustworthy LLMs daigoba66 · 71 pts · April 02, 2026 · 44% similar
- Terence Tao: Formalizing a proof in Lean using Claude Code [video] helloplanets · 51 pts · March 09, 2026 · 43% similar
- Entities enabling scientific fraud at scale (2025) peyton · 276 pts · March 11, 2026 · 42% similar
- Lf-lean: The frontier of verified software engineering alpaylan · 18 pts · March 12, 2026 · 42% similar
- Agents of Chaos pagade · 13 pts · March 07, 2026 · 40% similar
Discussion Highlights (2 comments)
leanexplorer
Code part of the project PhysLib (formerly PhysLean) - physics version of the project Mathlib. https://github.com/leanprover-community/physlib
throwaway81523
Well it's a physics paper. The math being wrong is almost a running joke. It's almost 100 years since quantum field theory was invented and that doesn't formalize so well either.