Predictions for 2025?

Stream: general

[Matthew Ballard]

Similar to #general > Highlights of 2024? participants shared their predictions for the next year.
Predictions for 2025

1. AlphaProof or Open-Source Alternatives:
   • Possible community access or open-source development of AI tools inspired by AlphaProof.

2. Mathematical Milestones:
   • Completion of the classification of semisimple Lie algebras.
   • Differential forms and De Rham cohomology landing in Mathlib.

3. Community Challenges:
   • Formalization of Morse Theory.
   • Advancements in differential geometry, smooth manifolds, and analytic spaces.
   • Development of Hodge structures and mixed Hodge theory in Mathlib.
   • Hope for new contributors formalizing partial differential equations and functional analysis.

4. Tooling and Technical Improvements:
   • Further scaling tools to handle increasing PR volume (e.g., 1,500+ pull requests per month).
   • Improvements in the Lean review process and dashboards.

5. AI in Mathematical Competitions:
   • Multiple AI entrants in events like the Math Olympiad, potentially using Lean for verification.

6. Infinity-Cosmos Project:
   • Progress expected on this initiative.

7. Broader Community Engagement:
   • Continued community expansion through workshops, teaching, and hidden research groups emerging globally.

[Matthew Ballard]

GPT-4o also took my joking suggestion of Lean 5 with Brian Conrad support seriously :)

[Matthew Ballard]

Please share your own expectations for the new year -- no constraint on wildness of speculation!

[Jason Rute]

I think Lean will be a major part of the business model for various startups, like Harmonic and Numina.

[Frederick Pu]

Hopefully there will be a metaprogramming benchmark for lean4 similar to miniF2F but for writing tactics, elaborators and parsers. As well as better tactic support for HEq and better pattern matching for well-founded recursive definitions.

[Jason Rute]

Are you offering to make one @Frederick Pu?

[Frederick Pu]

honestly I'd be down

[Frederick Pu]

there's defintely more than enough content on zulip

[Jason Rute]

Similarly to my other prediction above, I think AI for Lean (and Coq/Isabelle) will generate real tangible value in a number of use cases. The question is if it will be just proprietary industrial use cases or if it will also be for building Mathlib and other Lean math projects. I think that will be largely up to the Lean community.

[Frederick Pu]

maybe there'll be a separate lean for science repo like mathlib

[Jireh Loreaux]

I think there are some? At the very least there's HepLean

[Adam Topaz]

Who is planning to do Morse theory?!

[Johan Commelin]

It's a challenge!

[Daniel Weber]

I hope for an $\mathbb{R}$ game, both for constructing a complete linearly ordered field and for proving stuff about one

[Huajian Xin]

Jason Rute said:

I think Lean will be a major part of the business model for various startups, like Harmonic and Numina.

In fact, as far as I know, besides Numina and Harmonic, many other players have already entered the field, including universities, startups, and AI departments of large companies. They're just still operating under the radar for now. I believe 2025 will be a breakout year for LLMs for Lean.

[Michael Rothgang]

I'd like to add a challenge: some basics of singular homology are added to mathlib, e.g. leading up to the computation of homology of spheres.

(This was done in Lean 3 by @Brendan Seamas Murphy, but homological algebra was refactored a lot (for the better!) since then. This needs a hero to port/re-do this work with current mathlib.)

[Jireh Loreaux]

I want to see fun_trans in Mathlib this year @Tomas Skrivan :wink:

[Simone Melchiorre Chiarello]

Is anybody currently working on this, particularly on 3.? (mixed) Hodge structures could be defined purely algebraically, which does not seem such a hard task, however you need some differential geometry and cohomology theory to give some applications of Hodge theory, and such thing seems much more daunting. Is there any precise plan to tackle this?

[Kevin Buzzard]

Both differential geometry and cohomology theory are moving but very slowly because not enough people are working on them.

[Simone Melchiorre Chiarello]

Put like that, cohomology (thinking of De Rham and/or Dolbeault one) and differential geometry seem low hanging fruits. However the fact that there are few people could in turn be a consequence of the fact that such topics are not of great interest in the community (or is it a chicken-and-egg situation...?)

[Kim Morrison]

No, I think many people would be really excited to see progress here. They unlock many more levels. :-)

[Kevin Buzzard]

I don't know why but in practice the community has far more users focused on algebra than on differential geometry. This is a social phenomenon rather than anything else.

[Alok Singh]

Kevin Buzzard said:

I don't know why but in practice the community has far more users focused on algebra than on differential geometry. This is a social phenomenon rather than anything else.

I think at least part of it is the perception that computers are inherently about the finitary parts of math and analysis/geometry is infinitary

[Kevin Buzzard]

The sphere eversion project disproved that

[Alok Singh]

But do _they_ know that?

[Pietro Monticone]

Kevin Buzzard said:

I don't know why but in practice the community has far more users focused on algebra than on differential geometry. This is a social phenomenon rather than anything else.

I'm actively working on that. I hope to be able to bring good news in a about a month...