dreams of big projects

Stream: general

[Kevin Buzzard]

FLT has been the big project I've been dreaming of for years. What other big Lean projects do people dream about? I'm talking about big projects which would unarguably have high visibility and impact and which would perhaps attract new users?

Example: There is room for at least one more "Langlands program" type project I should think, for example something on geometric Langlands would be feasible given that the popular science blogs are already reporting on it when it's not even been refereed!

Non-example: I don't think that ABC would be a good example, despite there being a lot of noise about it, simply because of the high chance of failure.

[Jeremy Tan]

How about Keevash's existence theorem for Steiner systems?

[Shreyas Srinivas]

My easy answer : Algolib. A library of algorithms theory that uses a standardised notion of complexity computation of functions (using a generic query model), and encodes proofs of complexity and correctness of algorithms

[Shreyas Srinivas]

And to be able to bring it to a level where recent results can be formalised in a few weeks.

[Shreyas Srinivas]

Given the messy state of the algorithms literature, I expect this to be a tad bit more challenging than for math.

[Michael Stoll]

Closer to FLT: I've been toying with the idea of formalizing a proof of Mordell's Conjecture (see these slides from the Mordell Conference last year).

[Patrick Massot]

There are not so many theorems comparable to FLT in terms of public recognition. The obvious candidate in pure algebra is the classification of finite simple groups. I know that very few people here (probably nobody?) feel excited about finite group theory, but we cannot avoid discussing this topic from time to time. In geometry and topology, I think the only comparable result is Perelman’s proof of the Poincaré conjecture.

[Ruben Van de Velde]

Can we state the classification yet?

[Riccardo Brasca]

Ruben Van de Velde said:

Can we state the classification yet?

Stating the classification is probably a reasonable project. Even proving that all the groups are simple is not impossible. CC @Antoine Chambert-Loir

[Yaël Dillies]

A big project that's been on Bhavik and I's radar is Szemerédi's theorem. It's of course close to my heart because it's additive combinatorics, but it has also since inspired great advances in ergodic theory, model theory, and was the motivation behind the birth of higher order Fourier analysis. There are four-five categories of proofs, and every one of them would provide huge value to mathlib and the greater community if formalised.

[Michael Rothgang]

Riccardo Brasca said:

Ruben Van de Velde said:

Can we state the classification yet?

Stating the classification is probably a reasonable project. Even proving that all the groups are simple is not impossible. CC Antoine Chambert-Loir

Didn't the formal abstracts project have a statement of the classification (with lots of sorries, of course)? CC @Floris van Doorn who worked on this, I believe

[Pim Otte]

Along another axis: A web development framework, perhaps along the lines of IHP. I don't think the time is ripe for this. For one, it depends on development of the http library in core. The feasibility also dependes on how willing one is to use the FFI at some point.

The goal here would be to create a framework with an opinionated architecture (Event Sourcing/CQRS?) that is amenable to formalization, along with automation. Then users would just have to specify a data model and implement functions, and if those functions satisfy the constraints implied by the architecture, the theorems about integrated functionality could be easily derived.

[Patrick Massot]

That would be great indeed. But having the analogue of python’s requests library would already be a huge improvement to applicability in ordinary programming.

[Riccardo Brasca]

In my opinion if we want something that in some sense will make even more news than Fermat, the only possibility is to formally prove an open "big" conjecture. This already happened in certain field of course, but we are very far from being able to that in, say, algebraic geometry or analysis.

[Julian Berman]

Is #general > Robertson–Seymour theorem perhaps another example?

[Patrick Massot]

Riccardo, I’m sure Terry will let us know when he’ll prove existence of blow-up for Navier-Stokes so that we can help him formalize it. In the mean time I think formalizing Perelman’s proof of the Poincaré conjecture would still be nice.

[Chris Birkbeck]

Riccardo Brasca said:

In my opinion if we want something that in some sense will make even more news than Fermat, the only possibility is to formally prove an open "big" conjecture. This already happened in certain field of course, but we are very far from being able to that in, say, algebraic geometry or analysis.

Maybe one first formalises the (statements of the) millennium prize problems

[Riccardo Brasca]

Chris Birkbeck said:

Riccardo Brasca said:

In my opinion if we want something that in some sense will make even more news than Fermat, the only possibility is to formally prove an open "big" conjecture. This already happened in certain field of course, but we are very far from being able to that in, say, algebraic geometry or analysis.

Maybe one first formalises the (statements of the) millennium prize problems

Riemann should be very easy, right?

[Chris Birkbeck]

We have Riemann in mathlib IIRC

[Riccardo Brasca]

Ah yes, RiemannHypothesis

[Floris van Doorn]

The statement of the classification of finite simple groups was indeed done in Lean 3: https://github.com/formalabstracts/formalabstracts/blob/master/src/group_theory/classification.lean (with sorry's for proofs used in the definition of many groups)

[Martin Dvořák]

Complexity Zoo in a unified framework.

[Chris Birkbeck]

BSD would be fun, can also prove at least 66% of it :P

[Floris van Doorn]

Patrick Massot said:

In the mean time I think formalizing Perelman’s proof of the Poincaré conjecture would still be nice.

Roughly how many preliminaries go into that proof? Is it significantly easier than proving FLT?

[Jeremy Tan]

Julian Berman said:

Is #general > Robertson–Seymour theorem perhaps another example?

Check out my list of 100 theorems somewhere in the mathlib issues list. It has R–S in it

[Jeremy Tan]

Also in my 100: the Heawood conjecture (4CT for arbitrary closed surfaces)

[Ruben Van de Velde]

(Has anything happened to formal abstracts in the last years? It seemed like a cool idea)

[Jeremy Tan]

Of course, 4CT has already been formalised in Rocq...

[Jeremy Tan]

#6091

[suhr]

My dream project is an unusual one: to make mathematics accessible for people without formal math education. There's a gap between people formally trained in math and self-taught mortals (e.g. programmers). Lean could help to bridge this gap by allowing learning by doing.

As an extra, it would be nice if programmers were more familiar with formal methods. A lot of people perceive formal methods as something PhD level hard, which is rather unjustified.

[Oliver Nash]

If we're really talking big then I think Perelman's Theorem / proof of the Geometrisation Conjecture might be the highest profile. I note that the Poincaré Conjecture is still the only Millennium Prize Problem for which we have a solution. Oh Patrick already said this :man_facepalming:

[Kevin Buzzard]

For me personally it's currently the most convincing answer.

[Patrick Massot]

I don’t know enough about FLT to compare. But Perelman’s proof would be very far beyond anything we’ve done so far. It would mean fantastic progress for Lean and Mathlib.

[Yakov Pechersky]

Verified CUDA kernels and a verified autodiff package similar to jax

[Patrick Massot]

Since someone mentioned that Mathlib contains a statement of the Riemann hypothesis, do we want a statement of the three-dimensional Poincaré conjecture? It would be very easy to do.

[Michael Rothgang]

Don't we have that already? file#Mathlib/Geometry/Manifold/PoincareConjecture, proof_wanted SimplyConnectedSpace.nonempty_diffeomorph_sphere_three?

[Riccardo Brasca]

Ah, we should decide how to treat those things. As a def as in Riemann and FLT or as a proof_wanted?

[Riccardo Brasca]

In my opinion a def seems better, so one can prove foo implies "big theorem"

[Jireh Loreaux]

You can have both :wink:

def BigTheorem : Prop := ...

proof_wanted BigTheorem

[Shreyas Srinivas]

Here's a more concrete goal I am looking to accomplish this year (and collaborators to do this): To port this repo from Isabelle to Lean: https://github.com/mabdula/Isabelle-Graph-Library

This is still ambitious but would be of interest for CS theory folks

[Arthur Paulino]

A featureful, robust, reliable and efficient HTTP library

[Oliver Nash]

I think we even considered this but it fell through the cracks during review
Jireh Loreaux said:

You can have both :wink:

[A.]

A headline-grabbing project would be the one that forces an LLM into unerring accuracy.

[Antoine Chambert-Loir]

Regarding the classification of simple groups, here are things I would like to see done in the next few years.

• I have the impression that defining the geometric groups will require to have more linear algebra to be able to define all classical groups, over an arbitrary fields, and in their nonsplit forms.

• Defining the sporadic groups is a question of finite permutation groups. The books on the subject should be formalizable in full, and it should not be too hard to do so.

• Those books will prove that the relevant sporadic groups are indeed simple. What I did for the alternating group (not yet in mathlib) is to use the Iwasawa criterion, docs#MulAction.IwasawaStructure.isSimpleGroup, and this is a major tool.

• The geometric groups are more interesting: up to elementary modifications, the special linear and symplectic groups are simple over any field. Orthogonal groups are more subtle, the isotropic ones are also simple over any field (with some counterexamples), but not the anistropic ones (the orthogonal group over a real closed field is not simple when there are infinitesimals).

• Something related with simplicity is the classification of the maximal subgroups of these simple groups. For symmetric and alternating groups, this is the O'Nan-Scott theorem, with an important addition by Liebeck, Praeger and Saxl; for geometric groups, it's a theorem of Aschbacher. Indeed, knowing than some subgroups is maximal is a key to their simplicity.

[Andrew Yang]

About sporadic groups: moonshine is also a cool thing to have.

[Geoffrey Irving]

A. said:

A headline-grabbing project would be the one that forces an LLM into unerring accuracy.

We already have one AI safety result in this space (proving accuracy of a simple scalable oversight method) formalised in Lean (https://github.com/girving/debate) and we have an improved result that I am doing the Lean preparation for now (either Blueprint or formalisation). If someone is interested I’m happy to chat.

[Bhavik Mehta]

Yaël Dillies said:

A big project that's been on Bhavik and I's radar is Szemerédi's theorem.

An extension of this is the Green-Tao theorem, which is probably more famous. It uses Szemerédi, and uses it as a black box.

[Adam Topaz]

My vote: Milnor Bloch-Kato (I.e the Voevodsky-Rost theorem). Alternatively the proof of the Weil conjectures.

[Derek Rhodes]

• I would like to see a math department step up and offer a new undergraduate degree, where as now there are typically "Applied" and "Pure", there would be a "Formalized" track, where all undergraduate courses are done with a proof assistant.
• Documentation for best practices about how to build undergraduate libraries that wrap Mathlib that expose only foundational lemmas so learners can't exact? their way to solutions, so that there would be standard consistent interfaces for Undergrad.Algebra, Undergrad.Analysis, etc. Ideally those wrappers would be a collaboration by many educators to help lighten the load when it comes time to upgrade.
• A tool that can port lean4 to lean5, along with documentation, projects and books without much human intervention.
• Along the lines of what @suhr mentioned. There are many people around the world without access to universities who would like to do proof based math. There are lots of math courses on MOOCs, but none of them are proof based, yet (as far as I know).
• More public discussion about the future of Lean, perhaps collaboration in the style of khronos, which coordinates with industrial partners who pay for membership that grants them the right to participate in steering committees. Software engineering daily had an enlightening interview with techs from the vulkan 3d graphics group about how that sausage is made.

[Scott Carnahan]

People have mentioned Perelman's proof of the 3d Poincaré conjecture/geometrization, but the 4-dimensional case is also quite interesting, in part because the smooth and topological questions are not equivalent. Freedman's proof of the topological question was widely seen as completely incomprehensible for about 30 years, but the "Bonn seminar" seems to have helped clarify the argument. The smooth 4d case is still open as far as I know. Smale's proof (in TOP) for dimension at least 5 seems to be much more accessible.

[Patrick Massot]

Of course I agree all cases of the Poincaré conjecture are great pieces of mathematics that would be amazing formalizations. But only Perelman’s story would be stunning for non-mathematicians.

[Bjørn Kjos-Hanssen]

Ruben Van de Velde said:

(Has anything happened to formal abstracts in the last years? It seemed like a cool idea)

I think the problem is that until you prove the theorem, you're not really sure if you've stated everything correctly.

[Kim Morrison]

I'm not sure anyone seriously tried to launch it... I wouldn't discount the idea.

[Junyan Xu]

Floris van Doorn said:

The statement of the classification of finite simple groups was indeed done in Lean 3: https://github.com/formalabstracts/formalabstracts/blob/master/src/group_theory/classification.lean (with sorry's for proofs used in the definition of many groups)

See also #general > The state of finite simple groups @ 💬

[Rida Hamadani]

"After 3 decades of uncertainty, the proof of the snark conjecture is finally verified" would probably be an attention grabbing headline. Bhavik talks more about it here: #general > Help me sell Lean to my professor @ 💬

[Julian Külshammer]

To suggest some topic not to seek attention from the general public, but to attract people from different areas of mathematics: Hodge theory. It comes with many different aspects, of course geometric, but the ideas have been used to prove famous conjectures: Elias-Williamson's proof of the Kazhdan-Lusztig conjecture in representation theory, or Adiprasito-Huh-Katz's proof of Rota's log concavity conjecture for matroids.

[Ilmārs Cīrulis]

My personal answer --- formal definition of Javascript (or its subset, at least) with tools to do verification of scripts in Lean. I like to do mathy stuff with it, and it would be nice if I could remove as much bugs as possible by formal verification.

Not sure if it is big, but at least it is a dream.

[Chris Wong]

This might not be very big, but my dream project is formalizing Modern Tetris. There's a lot of research and theory around the game (example), but it's fragmented across many documents and chat threads, and might contain mistakes. A Lean/Verso library could address both problems.

[Mario Carneiro]

Why would you say that formalizing Javascript is not big? There is literally a project called "Everest" which is trying to tackle something smaller than JS. Web is hard

[Mario Carneiro]

unless you mean just the core language semantics and not the web APIs it supplies

[Chris Wong]

The core language is pretty complicated too. I think it would be a significant project for someone to take on by themselves.

[Jz Pan]

Antoine Chambert-Loir said:

What I did for the alternating group (not yet in mathlib) is to use the Iwasawa criterion, docs#MulAction.IwasawaStructure.isSimpleGroup, and this is a major tool.

So you have the proof that A_n is a simple group if and only if n = 3 or n >= 5 in Lean but is not PR in mathlib yet?

[Antoine Chambert-Loir]

Yes, in my Jordan project, but I need to merge mathlib and make it compile again.

[Ruben Van de Velde]

Are you interested in help with that?

[Jz Pan]

Ruben Van de Velde said:

Are you interested in help with that?

Maybe a few days later, I think that shouldn't be hard, as the typical proof in textbook is about half a page.

[Jz Pan]

Oh I mean extract the proof that A_n is simple...

[Antoine Chambert-Loir]

Actually, I have two proofs. One was in lean3 and is the textbook proof. The other one proves much more, hence is much more complicated, and is more or less new.

[Antoine Chambert-Loir]

https://arxiv.org/abs/2303.12404

[Tomas Skrivan]

Yakov Pechersky said:

Verified CUDA kernels and a verified autodiff package similar to jax

This is one of the goals of SciLean, well the verified part will come only after it is sufficiently fast and user friendly. If anyone wants to help towards this goal it would be nice to add cuBLAS bindings to LeanBLAS.

For writing kernels, I have a tactic that can take a lean expression like fun (x : ℝ) => x + x * exp x and produce e : CExpr

inductive CExpr where
  | bvar (n : Nat) | add (x y : CExpr) | mul (x y : CExpr) | neg (x : CExpr) | exp (x : CExpr) | ...

together with a proof that interpretation of e back to ℝ → ℝ produces the original expression fun (x : ℝ) => x + x * exp x. We can then write fast functions like map or reduce using CExpr, probably by utilizing and extending lean-alloy to generate corresponding shims from CExpr. Feel free to reach out if you are interested in working on this.

[Luigi Massacci]

While not quite in the same league of FLT or Poincaré, o-minimality of $\mathbb{R}_{an, exp}$ would be cool to have. It's a fairly landmark result in applied model theory, and o-minimality has garnered even more interest recently.

[Ruben Van de Velde]

Antoine Chambert-Loir said:

Yes, in my Jordan project, but I need to merge mathlib and make it compile again.

I didn't manage to stop myself from updating your code to latest stable: https://github.com/AntoineChambert-Loir/Jordan4/pull/1 :)

[Ilmārs Cīrulis]

Mario Carneiro said:

Why would you say that formalizing Javascript is not big? There is literally a project called "Everest" which is trying to tackle something smaller than JS. Web is hard

I just don't know if it is big enough compared to another dreams mentioned here. And it's done in Coq, I believe, so maybe porting it is an option. But there are no tools, as far as I know, like Verified Software Toolchain for C language in Coq, so it is, maybe, big in the end.
It also becomes not so big, if only subset of it is formalized, too.

Basically, I just don't know, is it big or not. Sorry. :sweat_smile:

[Ilmārs Cīrulis]

Ah, yes, I meant the language itself, without many additional things that's connected to it in the modern Web.

[Tyler Josephson ⚛️]

Markov Chain Monte Carlo, and the Metropolis-Hastings Algorithm, in particular. The basis of all simulations involving random numbers, from physics to chemistry to biology to Wall Street to Bayesian inference. Imagine if we could generate samples from a distribution, prove correctness of the algorithm generating the samples (conditions like detailed balance), and prove things about the distribution from which the samples are being drawn.

[Andrés Goens]

Just dreaming of a big project too, I would love to see Lean have the first bootstraped (self-hosted) verified compiler: usually it's a big milestone of a compiler when it is self-hosting, i.e. when it can compile itself. No compiler has ever been self-verifiying, i.e. it can check the proof of its own correctness.

This is different from, say Coq-in-Coq or Lean4Lean in that it's about the compiler, i.e. going from Lean to C or LLVM in the case of Lean, not the semantics of the core language. Of course you need the semantics of Lean to prove that they're preserved, so it builds up on this.

I think Lean has a nice advantage in that it's a small core language and most of it is defined in itself, so having a self-verified compiler is not impsosible. The main challenge would be of course that this kind of big project would have to either re-build/fork a lot of core in a separate project, or coordinate well with core/the FRO, but at this stage I'm just dreaming :)

[Eric Taucher]

@Kevin Buzzard

While this is not one one about creating a specific proof using Lean, it is something that Kevin has noted from time to time and would help many here.

The ability to convert a proof or algorithms in PDFs into Lean.

[Siddhartha Gadgil]

Patrick Massot said:

There are not so many theorems comparable to FLT in terms of public recognition. The obvious candidate in pure algebra is the classification of finite simple groups. I know that very few people here (probably nobody?) feel excited about finite group theory, but we cannot avoid discussing this topic from time to time. In geometry and topology, I think the only comparable result is Perelman’s proof of the Poincaré conjecture.

Does Lean have exotic spheres? How about exotic $R^4$s? The latter may be striking and not so hard given fully combinatorial versions of "Heegaard Floer theory" and friends. Closely related is the Milnor conjecture on unknotting number - may not be well known but not hard to explain.

[Patrick Massot]

Of course we have nothing like that.

[Patrick Massot]

And I don’t think you can get anywhere using only combinatorics. You can compute Heegaard-Floer using combinatorial methods, but then you need to relate the result to actual information.

[Alex Meiburg]

I think a proof of MIP*=RE would be awesome. Especially because some people still cast some doubt on it; putting it on firm footing would be great. It's a fairly deep proof. It doesn't have a lot of "consequences" for math in the particular sense that it mostly disproved some other nice conjectures, so it's not something that will be used in later proofs. Of course it had consequences for research and the state of math knowledge, but it's not something that will likely be needed for formalizing other theorems.

As a more tractable problem, I think a proof of Onsager's solution to the 2D Ising model would be a very nice mathematical result + derivation of a phase transition. This is something I vaguely hope to attempt sometime in the future...

[Winston Yin (尹維晨)]

I'd like to see foundational theories from a standard undergraduate physics curriculum formalised, to reproduce the success of the Xena Project. This includes Newtonian mechanics (free-body diagrams and laws of motion), classical electromagnetism (Maxwell's equations), thermodynamics and statistical mechanics, axiomatised quantum mechanics, and more.

To get some attention from working theoretical physicists, I dream of: the formalisation of Einstein's field equations, a few of its famous exact solutions (various black hole solutions in asymptotically Minkowski / dS / AdS space, FRW cosmology), and a few famous approximate solutions (gravitational waves). On the high energy physics side (@Joseph Tooby-Smith ), a geometric statement of the Yang-Mills Lagrangian and conformal field theory.

[Geoffrey Irving]

Winston Yin (尹維晨) said:

I'd like to see foundational theories from a standard undergraduate physics curriculum formalised, to reproduce the success of the Xena Project. This includes Newtonian mechanics (free-body diagrams and laws of motion), classical electromagnetism (Maxwell's equations), thermodynamics and statistical mechanics, axiomatised quantum mechanics, and more.

To get some attention from working theoretical physicists, I dream of: the formalisation of Einstein's field equations, a few of its famous exact solutions (various black hole solutions in asymptotically Minkowski / dS / AdS space, FRW cosmology), and a few famous approximate solutions (gravitational waves). On the high energy physics side (Joseph Tooby-Smith ), a geometric statement of the Yang-Mills Lagrangian and conformal field theory.

How about the Penrose-Hawking singularity theorems? :)

[Notification Bot]

Alex Meiburg has marked this topic as resolved.

[Notification Bot]

Alex Meiburg has marked this topic as unresolved.

[Alex Meiburg]

(oops)