3 ms·
What do you mean by not fully automatic? What is the manual part? I think right now the job of describing a (sophisticated) proof to a computer is analogous to
by tprice7 14y ago
What do you mean by not fully automatic? What is the manual part?
I think right now the job of describing a (sophisticated) proof to a computer is analogous to the job of writing a sophisticated computer program like a game or Facebook in assembly code. What mathematics needs is a concise language that can easily be understood by people and computers alike, like Python.
- foobarqux 14y agoThe manual part is writing out steps of the proof. Some times these steps can be automated. Usually they are guided by a user. They are typically not written out step by step by hand because it is very tedious. I doubt complicated ideas expressed in advanced mathematical papers can be easily or succinctly expressed formally. http://en.wikipedia.org/wiki/Theorem_prover http://en.wikipedia.org/wiki/Theorem_prover http://www.cs.ru.nl/~freek/100/ http://www.cs.ru.nl/~freek/100/ But more importantly, the objective of a mathematical paper is to get readers to understand the proof, a goal which is poorly achieved with formal verification.
- Evbn 14y agoHave you ever used one of these systems that you claim exists? Math is not mechanically formalized beyond a tiny bit of foundational set theory. Most of modern math is hand waving by brilliant people who trust each others hands, and Doron Zeilberger calling their bullshit and begging them to start being more careful.