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.