> 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 2 days ago | parent | next [-]

I 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 2 days ago | parent [-]

What 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 2 days ago | parent [-]

Deduce. So your #2.

▲

DoctorOetker 2 days ago | parent [-]

Of course a machine can verify each step of a proof, but that formal proof must be first presented to the machine.

▲

crazygringo 2 days ago | parent [-]

Right. 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 2 days ago | parent [-]

Theres 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 2 days ago \| parent [-]
		> 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 2 days ago | parent | prev | next [-]

For one, some geometric proofs by construction can literally involve pictures rather than statements, right?

	▲	DoctorOetker 2 days ago \| parent [-]
		Sure 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 2 days ago | parent | prev [-]

>Do you just mean that we must assume something to get the ball rolling

They're called "axioms"