Interesting article on progress in automated reasoning

[Alasdair Urquhart]

I've read this through a couple of times, and in general
it's a good semi-popular article on the subject.
Some of the assertions made by anti-computer people
are ridiculous.  For example, Michael Harris says:

“By the time I’ve reframed my question into a form that could fit into 
this technology, I would have solved the problem myself”

The article also implies that the proof of the four-colour theorem
is controversial (another assertion by Michael Harris).

A lot of the discussion on computer-assisted proofs fails
to distinguish between the high level heuristics in proofs
and the detailed verfications.  For example, in the 4CT,
there are high level probabilistic arguments that show
that the computer attack using the
methods of reducibility and discharging is overwhelmingly
likely to succeed.  For the details of this see the book
by Saaty and Kainen (Dover 1986), Section 3.6.
Of course, a verification is necessary, but the fact that
it has to be done by a computer is not surprising.

All in all, I recommend the article as a good overview.

Alasdair

On Mon, 6 Dec 2021, JOSEPH SHIPMAN wrote:

> Anyone want to comment on this?
> https://www.quantamagazine.org/how-close-are-computers-to-automating-mathematical-reasoning-20200827/
> 
> Sent from my iPhone