I think lean can verify it implements its own rules, but not that its own rules are sound (you can't prove a contradiction). If you are just prepared to trust that the rules are sound, then you would be able to trust leans implementation (if you had that Lean proof that it implements its own rules)

I think people on here tend to somewhat fixate on the determinism issue. Even with a deterministic LLM - stabilising the floating point arithmetic, and choosing from the distribution by a fixed method, or just save the random seeds - there is still a kind of a chaotic unpredictability that can exist between its inputs and outputs. However maybe that is a price that needs to be paid to get creativity.

Did any mathematics done by G H Hardy turn out to be quite useful in the end?

Ironically of course the answer is yes.

It's not really ironic. The fact that some mathematics is useful is not an argument or evidence that the goal of mathematics is utility.

It's also very risky to frame it that way, because that immediately leads to the idea that mathematical endeavors should be judged and funded according to their expected utility. That's product development, not research.

Yes indeed, it's about the time sound takes to travel 4mm

The dichotomy is more 'human understood' vs 'not human understood', I think

That was exactly my thought - taking out the problems that PhDs and early stage researchers work on kills the pipeline of developing mathematicians

It's an article written by a guest contributor - not an editorial written as the voice of the newspaper

Is the word "nonautological" autological ?

This is only the "problem solving" side of mathematics. Completely missing the theory builders who have completely reshaped the world of mathematics (and far beyond). AI is a long way from matching original thinkers of the calibre of Euclid, Al-Khwarizmi, Newton, Leibniz, Euler, Galois, Riemann, Cantor, Hilbert, and Grothendieck. Or Turing, Gödel and Von Neumann?

According to Tao and Gowers there are AI results that did proofs in clever ways. That’s one way new theories come about.