Non-trivial error in physics paper found via Lean
leanexplorer
21 points
2 comments
March 22, 2026
Related Discussions
Found 5 related stories in 71.1ms across 8,303 title embeddings via pgvector HNSW
- ML supports existence of unrecognized transient astronomical phenomena solarist · 65 pts · April 24, 2026 · 45% similar
- Computational Physics (2nd Edition) (2025) teleforce · 126 pts · April 05, 2026 · 45% similar
- The case for zero-error horizons in trustworthy LLMs daigoba66 · 71 pts · April 02, 2026 · 44% similar
- PyTorch simulator refutes an 18-year-old quantum theorem NeoOdim · 16 pts · May 14, 2026 · 43% similar
- Terence Tao: Formalizing a proof in Lean using Claude Code [video] helloplanets · 51 pts · March 09, 2026 · 43% 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.