4 ms·
> we can't automate the math, yet This exists: https://en.wikipedia.org/wiki/Automated_theorem_proving https://en.wikipedia.org/wiki/Automated_theorem_proving
by dharmaturtle 5y ago
> we can't automate the math, yet
This exists: https://en.wikipedia.org/wiki/Automated_theorem_proving https://en.wikipedia.org/wiki/Automated_theorem_proving
- bccdee 5y agoThis is moreso automation-assisted theorem proving. It takes a lot of human work to get a problem to the point where automation can be useful. It's like saying that calculators can solve complex math problems; it's true in a sense, but it's not not strictly true. We solve the complex math problems using calculators.
- sterlind 5y agoand there's already GPT-f [0], which is a GPT-based automated theorem prover for the Metamath language, which apparently submitted novel short proofs which were accepted into Metamath's archive. I would very much like GPT-f for something like SMT, then it could actually make Dafny efficient to check (and probably avoid needing to help it out when it gets stuck!) 0. https://analyticsindiamag.com/what-is-gpt-f/ https://analyticsindiamag.com/what-is-gpt-f/
- IAmLiterallyAB 5y agoSomeone tell Gödel