What do you (yes, you) hope to achieve with Lean in 2025?

Stream: general

[Ilmārs Cīrulis]

(I hope this topic is different enough from topic Predictions for 2025. :sweat_smile: )

1) What you plan and/or hope to achieve in 2025, using Lean?
2) Happy Holidays! :)

[Ilmārs Cīrulis]

• I plan to prove the correctness of the solution of Project Euler 3rd problem: see here
• I also plan/hope to start tinkering with SimpleGraph again, from very beginnings with something simple towards, dunno, as complex as I can afford. Better to be slow but stable (?), probably.
• I hope to start some standard functional programming, using Lean, and make some tiny working software maybe.
• And maybe something else too. It's probable (maybe some p=0.25) that I start studies in math September 2025, then I will try to do all the math using Lean, at least until it maybe becomes too hard.

Ok, that's all! Happy Holidays and Happy 2025! :happy:

[Kevin Buzzard]

I hope to have understood far better, by the end of 2025, just how hard it is to formalize the proof of "[big list of hard theorems proved in the 1980s] -> Fermat's Last Theorem". I am entertaining the idea more and more that by the end of 2025 we will have made substantial progress towards this. Initially my argument that this "must be hard" was "if we can do this then we must have formalised the Wiles and Taylor/Wiles papers in some form or other, and this is hundreds of pages of mathematics so it must be hard" but now I am looking at what actually needs to be done and thinking "do you know what, this doesn't seem too bad". One switch in mindset I've had is that I am generating lots of preliminary work and leaving lots of sorrys for other people (or for me later on) but all these sorrys were certainly known in the 1980s, so if by the end of 2025 we have 200 open issues on the FLT repo but all of them correspond to mathematics known in the 1980s then, at least for the initial goal I've set out to prove, this doesn't matter.

[Ruben Van de Velde]

Get Lindemann Weierstrass landed :sweat_smile:

[Yaël Dillies]

I think the biggest threat with the FLT project is that Andrew will get it done in a few months and then be out of a job for his PhD :laughing:

[Huajian Xin]

In 2025, I hope that the specialized LLMs we LLM developers create for Lean theorem proving can truly be of help to all of you—the contributors in the Lean community—whether in a form similar to ChatGPT, GitHub Copilot, or something like Cursor. Connecting machines with humans has always been the ultimate goal for us, the developers of these machines. :smile:

[Ruben Van de Velde]

I think we then say "1980s? We meant 1960s"

[Frederick Pu]

hopefully have some sort ai based refactoring and metaproggraming capabilities. so that we can feed in a paper and get a bunch of preliminary definitions that can be distilled and refactored by us soup computers

[Frederick Pu]

on that I want to make miniF2F but for metaproggraming and have a library for writing certified parsers

[screentime]

1. Learn how Lean formalizes the basic topics of undergrad maths. Get some practice doing proofs with those topics.
2. Learn how Lean works under the covers (questions like what's the architectural picture, when does computation happen, etc.). Or if that's too much/hard, learn how to learn about this (questions like how to trace what's going on inside Lean as I ask it to do something).
3. Learn a bit more about the proof assistant, type theory, foundations, etc. landscapes. Like how Lean contrasts with Agda, why we opted to use type theory instead of set theory, and how the different type theories interact.
4. Implement a toy dependent type system, and figure out how to map some Lean concepts onto it.

[Jireh Loreaux]

My goal for 2025 is to recruit more people in operator algebras to Lean and help them become proficient contributors to the formalization of the subject.

[Edward van de Meent]

i hope to get my free probability project (aiming for the free version of CLT) done and in shape to merge in mathlib

[Adam Topaz]

$\pi_1^{\mathrm{et}}(\mathbb{P}^1\setminus\{0,1,\infty\})$ ;)

[Shreyas Srinivas]

My goal is to finally publish the stuff that I have been building up in lean for the last 1.5 years in various pieces of TCS, especiallt algorithms theory. Things are already beginning to look bright, in the sense that I am beginning to see simpler proof expositions than I find in the literature in a few places. I also predict that in 2025, we might see the first formalises papers in algorithms conferences in general.

But I am also not too keen to count my chickens before they hatch.

[Chris Henson]

As part of my candidacy exam, I am formalizing the categorical semantics of a few lambda calculi. If I get things in good enough shape, I'll consider a PR with hyperdoctrines and maybe CWFs as my first Mathlib contribution.

For Advent of Code, I started porting Rust's pathfinding crate. I might put this up on my GitHub as a package after I clean things up a bit. I've been thinking a lot first about if I want to replicate their approach of using hashmaps that preserve insertion order and how to handle termination.

[Frederick Pu]

express procedural languages such as C as a monad M. Then write an elaborator that elaborates C syntax into that monad M so that we can use leans do notation to construct ad-hoc dafney style proofs

[Markus de Medeiros]

One of my goals is to build a program logic in Lean. Hopefully, this will help me understand any technical differences between Lean and theorem provers with more longer histories in program verification like Rocq (I'm looking at you, generalized rewriting ;))

[Miguel Marco]

I am doing a lean game that follows my general topology course. I plan to finish it in the following months, and use it as additional material for the course in the next academic year (maybe grant some extra points to the students that finish it).

[Julian Berman]

I'll probably be trying to:

• make lean.nvim feel even more polished so that a few more people use it
• write some more meaningful programming library for Lean -- possibly returning to a JSON Schema implementation or to embedding PyPy in Lean, or possibly trying to write something like a magic wormhole implementation
• Continue looking for a small piece of math I can learn enough to contribute to FLT in some tiny way

[Floris van Doorn]

With help from others:

• Finish the Carleson project
• Port a good part of it to Mathlib
• Start a new project formalizing research-level harmonic analysis

[Scott Carnahan]

Construct the monster vertex algebra (and its automorphism group).

[Joseph Myers]

I hope to make more progress on AperiodicMonotilesLean, moving beyond setting up background definitions and API for tilings to things more directly related to the actual proofs of aperiodicity, as well as starting to PR the background definitions and API to mathlib.

I also hope to expand the mathlib coverage of geometric definitions and API needed to at least state a greater proportion of past IMO problems idiomatically, if no-one else gets the relevant definitions and API into mathlib first.

[Quang Dao]

I hope to fully formalize succinct non-interactive arguments (SNARKs) this year. If finished, this will be a large-scale formalization of an important cryptographic primitive with practical impacts (lots of money on blockchains rely on these proof systems being sound).

I also hope to avail myself of any AI tool that can speed up this formalization project. So far cursor has been helpful in making routine edits, but it would be nice to have a more integrated tool that can prove non-trivial theorems

[Daniel Weber]

I hope to finish contributing to mathlib the proof that the error function isn't elementary

[Greg Shuflin]

I'm really interested in using Lean for ordinary software engineering tasks, with judicious use of the theorem-proving functionality in ways that eliminate the possibility of classes of bugs in a pretty concrete, user facing way.

In particular I'd like to try to use lean to:

1. write tooling that can interact with Git repositories
2. computer graphics, and in particular setting as a goal writing an implementation of Tetris in Lean (and ultimately, maybe even some original games)

[Martin Dvořák]

I want to complete the easy direction of #announce > Regular Matroid Decomposition Theorem next year.

[Jason Rute]

I plan, even if it is just on my own time, to get a better sense of what are all the AI tools currently available for Lean. How does one install them? How does one use them? How does one make simple improvements to them? And in what situations are they useful? (I don’t think I have a lot of time for this given my other work and life responsibilities, so I’d also love for others to take this on as well.)

[Joseph Tooby-Smith]

My goal is to get more people involved in HepLean, from both the Lean and physics communities. In particular, I plan on developing the necessary infrastructure and foundations to make this easier.

[Michael Rothgang]

• (perhaps still in 2024) show a better "last updated" value in the mathlib review and triage dashboard
• contribute to the Carleson project
• (with Yury Kudriashov) formalise Moreira's version of Sard's theorem, PR it to mathlib
• ensure Morse-Sard's theorem on manifolds lands in mathlib
• perhaps: define Sobolev spaces and prove the Sobolev embedding theorem
• perhaps: some fun differential geometry project, such as defining Riemannian metrics
• (with others) create a German version of lean-verbose and use it for teaching math first-years

[Violeta Hernández]

Right now my plans are to:

• Finish all my ordinal refactors so people stop complaining :stuck_out_tongue:
• (With help of others) get combinatorial game theory into a more workable place, and start formalizing some actual games!
• Prove nimbers are algebraically complete
• Potentially, start learning about PCF theory and get it into Mathlib

[Dominic Steinitz]

1. Recreate my blog post about the Mercator projection as a connection (thus straight lines are different from the shortest distance and the connection has torsion).
2. Principal bundles, connections as differential forms, curvature as a differential form, Einstein's equation via Cartan (is this even possible?), gravitational waves (lol)
3. Brownian motion, Black-Scholes

[Ayhon]

I want to explore Lean for program verification, in particular using the aenas Rust verification toolchain to verify a SPHINCS+ implementation, and try to use macros/automation to streamline the process for the verification of other cryptographic algorithms / programs.

Also, the creator of kyo, an effect system for Scala, has shown interest in formalizing the kernel of kyo, so I'd love to make a meaningful contribution to that project in Lean.