kevinbuzzard

Indeed I was being slightly tongue-in-cheek -- but if you ask geometers whether they believe the Hodge conjecture then you certainly don't always get an unqualified "yes"! This is in contrast to e.g. asking number theorists whether they believe Birch--Swinnerton-Dyer, where they are almost always very confident.

A discussion by Boris Alexeev on recent events in AI + mathematics

That is correct, the title is currently misleading (arguably the title of every paper I ever wrote was misleading before I finished the work, I guess, and the work linked to above is unfinished). If you are interested in seeing more details of the proof I'll be following, they are here https://web.stanford.edu/~dkim04/automorphy-lifting/ . This is a Stanford course Taylor gave this year on a "2025 proof of FLT".

Right now I would say that tools like Lean are not useful for learning advanced mathematics, currently you're mostly better off with pencil and paper. This might change but right now the infrastructure/tools aren't there to make experimenting with new and advanced concepts any easier than it would be on pen and paper.

Most mathematicians aren't doing formalization themselves, but my impression is that a lot of them are watching with interest. I get asked "is my job secure?" quite a lot nowadays. Answer is "currently yes".

Indeed. I'm not formalising FLT because I think it might be wrong -- I'm formalising it because I know the proof is correct, and using the project as an excuse to get some modern number theory into Lean's mathematics library. My hope is this will increase the chances that systems like Lean will one day be able to help modern mathematicians.

(I'm the author of the game) Unfortunately it did not. That comment was made when I was optimistic that an undergraduate who'd added more levels as a summer project would go on to PR them, but then the term started and they were distracted by their degree. We have some kind of prototypes for even/odd world (e.g. "prove odd * even is even") and prime number world (boss level: prove 2 is prime), plus a hard world consisting basically of unsolved problems such as Goldbach, Twin Prime Conjecture etc. But they never made the transition from "lean file containing a bunch of theorems" to "lots of files each containing one theorem and some rambling".

(I'm the author: yes, it was beta tested on many Imperial College London mathematics undergraduates)

I see! So I guess the proof of the pudding will be in the eating :-) Can you do algebraic geometry?

Right now, machines proving stuff which is interesting to lots of human mathematicians but unprovable by them is science fiction. People seem to have very different opinions on the following two questions:

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 highly doubt that the proof will get small enough to fit into a margin, but history shows that it's not at all unreasonable to expect simplifications/generalisations of the argument to come out of a formalisation (for example this happened with the Liquid Tensor Experiment, where dependence on stable homotopy groups of sphere was completely removed from the argument). I think it is unreasonable to expect that at the end of an FLT formalisation there will be no mention of elliptic curves, modular forms, Galois representations etc (the standard tools used by Wiles to prove the result in the 90s and which have themselves been simplified and generalised by mathematicians such as Taylor and Kisin since then). And you'll need quite a big margin to get all that stuff in.

Lean is free and open source and nothing to do with MS. Check out https://lean-lang.org/ and https://github.com/leanprover/lean4 -- no mention of MS or MSR (where de Moura was where he developed Lean 3 and started on Lean 4).

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".

My impression is that some parts of maths work best using set theory, some parts work best using type theory, some work best using a category-theoretic foundation and ignoring size issues etc etc. There's no one "best" foundations, and mathematicians on paper just freely (and mostly unknowingly) switch between foundations depending on what they're doing. This is problematic for a project such as formalising FLT because it involves developing mathematics in a bunch of different areas (algebra, analysis, geometry) where different foundations might be more appropriate (for example getting homological algebra working in dependent type theory has been annoying and hard for all the wrong reasons, and it's taken the Lean community years to figure out how to do it).

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.

Do we really know for sure that GPT4 has not seen this problem already?

Here's a Lean 3 development of a bunch of topos theory https://github.com/b-mehta/topos/tree/master/src , but it's not in the maths library (and now needs to be updated to Lean 4, although the community have had great success with that kind of project; one million lines of mathlib was translated from Lean 3 to Lean 4 using a combination of automation and human work)

Yes. Coq has been around for decades and was adopted by the software verification community. Lean is much younger and its mathematics library caught on with the mathematician crowd, meaning that much of the Lean documentation right now is focused on mathematics. The hitchhiker's guide to logical verification https://cs.brown.edu/courses/cs1951x/static_files/main.pdf is a book more suited for programmers, although it is in Lean 3 and right now the community is migrating to Lean 4.

Just to add my usual disclaimer: the mathlib project is a big open source project and I'm not its leader or even a maintainer of the code base. I am a contributor (as are hundreds of other people) and I talk about it a lot because I think it has the potential to change mathematics. But it is coordinated by many people, like many open source projects.

I just confirmed with Azerbayev that the typo in the example from Munkres ("identify" not "identity") was indeed what was fed to the algorithm (and the algorithm got it right anyway). We found some other funny examples when asking Lean to write strange definitions of differentiation: it would sometimes just write the correct definition (in correct Lean) despite being asked to write something else, perhaps because it has seen the correct definition far too often? It's pretty weird to play with!

PS I cannot believe my undergraduate teaching material is on HN! I am a math lecturer and this is just my course notes for my UGs.

Thanks so much! Fixed.

The fact remains though that Lean 3 worked well enough to do Scholze level mathematics. I never quite know what to make of people saying "if the designers had done it in some other way, it would have been better". Of course if someone comes along doing it another way, and then they go on to also achieve Scholze level mathematics, then I will be all ears.

Defeq undecidability is a feature of Lean in the sense that it is a conscious design decision. As we have seen both in this thread and in other places, this design decision puts off some people interested in the foundations of type theory from working with Lean. However it turns out that for people interested other kinds of questions (e.g. the mathematics of Scholze), defeq undecidability is of no relevance at all.

Here's an analogue. It's like saying "Goedel proved that maths was undecidable therefore maths is unusable and you shouldn't prove theorems". The point is that Goedel's observation is of no practical relevance to a modern number theorist and does not provide any kind of obstruction in practice to the kind of things that number theorists think about.

I'm not quite sure what you're asking about. I'm saying that we can't yet take the Wiles and Taylor-Wiles proof of Fermat's Last Theorem, feed it into a machine, and get a Lean proof of Fermat's Last Theorem.

Lean and the other theorem provers turn mathematical proofs into levels of a computer puzzle game, much like a chess puzzle.

Presumably the asterix denotes "actually true"? ;-)

I agree, but I think my statement is accurate today in 2021. I would love to see funds directed towards this sort of question. The big problem is that at high level so so much is skipped over, and you still sometimes have to struggle to put undergraduate-level mathematics into Lean -- this is why UG maths is such a good test case.

Basically it turned out that theoretical undecidability did not matter in practice, because Scholze mathematics relies so little on definitional equality. We prove theorems with `simp` not `refl`. Pierre-Marie Pédrot is quoted above as saying that various design decisions are "breaking everything around", but we don't care that our `refl` is slightly broken because it is regarded as quite a low-level tool for the tasks (eg proving theorems of Clausen and Scholze) that we are actually interested in, and I believe our interests contrast quite a lot with the things that Pédrot is interested in.

It's mathematics where certain kinds of proof by contradiction are not allowed -- if you want to prove that something exists because you want to use it, then you have to make it, you can't just say "let's assume it didn't exist and go on from there to deduce that 0 = 1 which is definitely wrong, so our assumption is wrong, so it exists, so let's use it".

Here is the reason why it's obvious for mathematicians. If you're trying to prove a theorem (e.g. the theorem that class numbers of imaginary quadratic fields tend to infinity), and then someone comes up with a proof which assumes that a certain generalisation of the Riemann hypothesis is true, and then someone else comes up with a proof which assumes that the exact same generalisation is false, then we mathematicians say "great, the theorem is now proved". This actually happened.

However if your boss asks you to write some code which does a calculation, and the next day you show up in their office with two USB sticks and say "this code is guaranteed to produce the correct answer if the Riemann hypothesis is true, and this other code is guaranteed to produce the correct answer if the Riemann hypothesis is false" then you are going to lose your job, because all you did was prove that the code exists, which is less helpful than it could be.

For me one of the biggest problems with the area of formalisation of mathematics is that for decades it has been dominated by computer scientists, whose view of what is important and beautiful in mathematics does not really coincide with that of the working mathematician. This is what I am fighting to change.

:-) Yes, by assuming classical logic the Lean community is taking a non-classical approach to bringing formalisation to the masses :-)

This is a milestone result, and its formalisation taught us many things, for example that the systems are capable of handling long proofs about elementary objects.

However finite graph theory is not remotely mainstream mathematics. Take your favourite super-prestigious maths prize, for example the Abel Prize or the Fields Medal. Now look at everyone who has won this prize in the last 10 years. That is the definition of mainstream mathematics. And as you will see if you do this, the areas which these people are working on are a million miles away from finite graph theory. This is precisely the problem. Computer scientists sometimes have a very twisted view of exactly what kind of mathematics is regarded as important in 2021. The experiment I outline above will give you some idea of what is mainstream, and believe me, it's not the four colour theorem.