Non-trivial error in physics paper found via Lean

Y	Hacker News new \| ask \| show \| jobs

	Non-trivial error in physics paper found via Lean (arxiv.org)
	24 points by leanexplorer 132 days ago

2 comments

leanexplorer 132 days ago

Code part of the project PhysLib (formerly PhysLean) - physics version of the project Mathlib.

https://github.com/leanprover-community/physlib

link

throwaway81523 131 days ago

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.

link