4 ms·
Plus, mathematics isn't just a giant machine of deductive statements. And the proof checking systems are in their infant stages and require huge amounts of effo
by bmitc 10mo ago
Plus, mathematics isn't just a giant machine of deductive statements. And the proof checking systems are in their infant stages and require huge amounts of efforts even for simple things.
- RossBencina 10mo ago> mathematics isn't just a giant machine of deductive statements I think the subject at question here is mathematical truth, not "mathematics" whatever that means.
- sublinear 10mo ago> mathematics isn't just a giant machine of deductive statements I know HN can be volatile sometimes, but I sincerely want to hear more about these parts of math that are not pure deductive reasoning. Do you just mean that we must assume something to get the ball rolling, or what?
- crazygringo 10mo agoI think the point was that it's not a machine. Stuff that we can deduce in math with common sense, geometric intuition, etc. can be incredibly difficult to formalize so that a machine can do it.
- DoctorOetker 10mo agoWhat do you mean with "do it" in "...etc. can be incredibly difficult to formalize so that a machine can do it." ? 1. do it = search for a proof 2. do it = verify a purported proof?
- crazygringo 10mo agoDeduce. So your #2.
- DoctorOetker 10mo agoOf course a machine can verify each step of a proof, but that formal proof must be first presented to the machine.
- crazygringo 10mo agoRight. And I said it's incredibly difficult to formalize so that a machine can do it. I don't understand what you're confused about.
- DoctorOetker 10mo agoTheres nothing difficult about formalizing a proof you understand. Formalizing hot garbage supposedly describing a proof can be arbitrarily difficult. The problem is not a missing library. The number of definitions and lemmas indirectly used is often not that much. Most of the time wasted when formalizing is discovering time and time again that prior authors are wasting your time, sometimes with verifiably false assumptions, but the community keeps sending you around to another gap-filling approach.
- crazygringo 10mo ago> Theres nothing difficult about formalizing a proof you understand. What are you basing that on? It's completely false. If that were true, we would have machine proofs of basically everything we have published proofs for. Every published mathematical paper would be accompanied by with its machine-provable version. But it's not, because the kind of proof suitable for academic publication can easily take multiple years to formalize to the degree it can be verified by computer. Yes of course a large part depends on formalizing prior authors' work, but both are hard -- the prior stuff and your new stuff. Your assertion that there's "nothing difficult" is contradicted by all the mathematicians I know.
- pxc 10mo agoFor one, some geometric proofs by construction can literally involve pictures rather than statements, right?
- DoctorOetker 10mo agoSure the history of mathematics used many alternative conceptions of "proof". The problem is that such constructions were later found to be full of hidden assumptions. Like working in a plane vs on a spherical surface etc. The advantage of systems like MetaMath are: 1. prover and verifier are essentially separate code bases, indeed the MM prover is essentially absent, its up to humans or other pieces of software to generate proofs. The database just contains explicit axioms, definitions, theorems claims, with proofs for each theorem. The verifier is a minimalistic routine with a minimum amount of lines of code (basically substitution maps, with strict conditions). The proof is a concrete object, a finite list of steps. 2. None of the axioms are hardcoded or optimized, like they tend to be in proof systems where proof search and verification are intermixed, forcing axioms upon the user.
- variaga 10mo ago>Do you just mean that we must assume something to get the ball rolling They're called "axioms"