Non-trivial error in physics paper found via Lean

(arxiv.org)

23 points | by leanexplorer 2 days ago ago

2 comments

  • throwaway81523 2 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.

  • leanexplorer 2 days ago

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

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