Interesting article on progress in automated reasoning

[Sam Sanders]

Dear Aladair,

> Some of the assertions made by anti-computer people
> are ridiculous.  

If you use the dictionary definition (ridiculous = deserving or inviting derision or mockery; absurd)
then I personally disagree with your claim, for the following reason.

> 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”

This is not a ridiculous statement if 

1) one is thinking of formalising e.g. analysis,

2) one is not used to serious/every-day programming (where LaTeX does not count).

There are a number of mathematicians satisfying conditions 1) and 2).  

To be more precise, for many people there is a steep learning curve involved in formalising mathematics, 
while just getting everything installed on one’s computer is already non-trivial.   

As a personal example, as recently as 2019, I could not get a real answer to the question

“How do you define open sets (in formalised math)?”

The answer was always:

“What do you want to do?”

This is not exactly helpful in bringing people to The Cause.  

My point is that novices and specialists have a lot of trouble 
talking to each other (as is often the case), and one should not 
immediately dismiss the qualms of either as ‘ridiculous’.

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

That is indeed absurd, unless arguments were given.  

> A lot of the discussion on computer-assisted proofs fails
> to distinguish between the high level heuristics in proofs
> and the detailed verfications.  

That is indeed a good point.  

Best,

Sam