Hacker news

  • Top
  • New
  • Past
  • Ask
  • Show
  • Jobs

Non-trivial error in physics paper found via Lean (https://arxiv.org)

20 points by leanexplorer about 15 hours ago | 2 comments | View on ycombinator

throwaway81523 about 3 hours 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 about 15 hours ago |

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

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