Understanding IMO is "developing a correct mental model of a concept". Some heuristics of correctness:

Feynman: "What I cannot build. I do not understand"

Einstein: "If you can't explain it to a six year old, you don't understand it yourself"

Of course none of this changes anything around the machine generated proofs. The point of the proof is to communicate ideas; formalization and verification is simply a certificate showing that those ideas are worth checking out.

▲

practal 3 hours ago | parent [-]

Ideas and correctness depend on each other. You usually start with an idea, and check if it is correct. If not, you adjust the idea until it becomes correct. Once you have a correct idea, you can go looking for more ideas based on this.

Formalisation and (formulating) ideas are not separate things, they are both mathematics. In particular, it is not that one should live in Lean, and the other one in blueprints.

Formalisation and verification are not simply certificates. For example, what language are you using for the formalisation? That influences how you can express your ideas formally. The more beautiful your language, the more the formal counter part can look like the original informal idea. This capability might actually be a way to define what it means for a language to be beautiful, together with simplicity.

▲

mutkach 3 hours ago | parent [-]

I share your fascination with proof assistants and formal verification, but the reality is that I am yet to see an actual mathematician working on frontier research who is excited about formalizing their ideas, or enthusiastic about putting in the actual (additional) work to build the formalization prerequisites to even begin defining the theorem's statement in that (formal) language.

▲

practal 2 hours ago | parent | next [-]

You know what? I agree with you. I have not formalised any of my stuff on abstraction logic [1] for that reason (although that would not be too difficult in Isabelle or Lean), I want to write it down in Practal [2], this becoming possible I see as the first serious milestone for Practal. Eventually, I want Practal to feel more natural than paper, and definitely more natural than LaTeX. That's the goal, and I feel many people now see that this will be possible with AI within the next decade.

[1] http://abstractionlogic.com

[2] https://practal.com

▲

hollerith 3 hours ago | parent | prev [-]

>I am yet to see an actual mathematician working on frontier research who is excited about formalizing their ideas

British mathematician Kevin Buzzard has been evangelizing proof assistants since 2017. I'll leave it to you to decide whether he is working on frontier research:

https://profiles.imperial.ac.uk/k.buzzard/publications

	▲	mutkach 2 hours ago \| parent [-]
		Sure, he is one of biggest advocates for it, and yet he was quite clear that it is not yet possible for him to do his actual research in Lean. Quoting one of the recent papers (2020): > With current technology, it would take many person-decades to formalise Scholze’s results. Indeed, even stating Scholze’s theorems would be an achievement. Before that, one has of course to formalise the definition of a perfectoid space, and this is what we have done, using the Lean theorem prover.