Comments URL: https://news.ycombinator.com/item?id=46162295

Points: 7

# Comments: 1

1) Whether it will still be science fiction by 2030;

2) Whether ITPs like Lean will be useful when working on this goal, or whether it will just be LLMs all the way.

But rather than asking questions like "will some system belch out a million line incomprehensible proof of the Riemann Hypothesis" one could ask the following much easier question. Computers are very helpful to mathematicians who do calculations right now, but are way way less helpful to mathematicians who prove theorems (there are many pure mathematicians in my department who have absolutely no use for computers in their research other than the obvious email/search/etc applications). Can we make tools which will help these mathematicians (who might be trying to prove theorems about uncountable and noncomputable objects) to do their day job? Again one can ask two questions:

1) Will this still be science fiction in 2030;

2) Will ITPs be involved?

And again I don't know the answers, but this work is an attempt by the Lean community to help ITPs understand precise statements of what's going on in modern number theory, in case that helps with (1).

I have no doubt that a similar project could be done in Coq. The fact that we're using Lean is a random historical coincidence. If we'd used Coq then you could ask "why not Lean".

So I don't really understand the point made in this post. Dependent type theory makes the expression of some theorems more involved and complicated -- but set theory makes the expression of some other theorems more involved and complicated, simple type theory makes the expression of some others more involved etc etc. You're right that we're just powering through this: but formalising mathematics in Lean sometimes feels like fighting against type theory (and sometimes type theory is a very welcome foundation). The point really is that the Lean community, because of its viewpoint of "formalise all mathematics in one system", has been forced to figure out how to power through the areas where dependent type theory was not the ideal foundation. Maybe the same can be said of Mizar and set theory -- I'm unclear about how much formalisation in Mizar is motivated by "let's do this because it will be unproblematic in set theory" and how much is "let's choose to do battle with set theory". In mathlib we've decided to do everything so doing battle with dependent type theory is a necessary consequence. I find it hard to believe that another foundational choice (such as Practal) solves these sorts of problems: presumably what's actually true is that some stuff which is annoying in Lean is nice in Practal but some other stuff which is nice in Lean is annoying in Practal.