Loogle: a search tool for Lean/Mathlib. https://loogle.lean-fro.org #ITP #LeanProver #Mathlib

If you're excited about this sort of thing, there's plenty of ways to contribute. For example, you could pick an undergrad-level subject that is not yet in #mathlib (Lean's giant proof library) and formalize relevant structures & theorems: https://leanprover-community.github.io/undergrad_todo.html

Formalizing the change of variables formula for integrals in mathlib. ~ Sébastien Gouëze. https://bit.ly/43qC2BB #ITP #LeanProver #Mathlib #Math

Recently, I have been interested in Lean, a theorem prover. Specifically, I’m intrigued by its community-written maths library for it, mathlib! Let me give a short introduction.

A theorem prover is very simple. It starts with certain axioms, and proves statements that are consistent with them! Of course, we are not at the point of AI auto-generating such proofs yet (though Tim Gowers’ work seems interesting). However, we as humans can still write proofs that the compiler and kernel VM can check.

In the 2-3 weeks I have been involved so far, I find the language to be quite accessible, even for mathematicians! Despite the community still being quite small, it is rapidly growing, with Kevin Buzzard and others even teaching it to undergraduates. Of course, as more people join in, more people can contribute to different areas, which will accelerate formalising more parts of maths.

Also, it is already well developed to the point where several famous proofs have been verified. Things like formalising the definition of perfectoid spaces, the proof of a density conjecture about unit fractions (involving sieve methods and some fourier analysis) and gallagher’s ergodic theorem, all of which are in some sense “modern” maths.

That’s why I think you should join too! It requires very little time to pick up, and once you get used to the syntax, it is quite similar (though a bit slower and more verbose) to writing your normal maths proofs. I am mainly working on Analytic number theory (which is quite lacking in mathlib, or complex analysis in general), though I might considering branching to Ergodic theory and Additive combinatorics if I feel like so. Feel free to contact me if you want to work on something together!! I have some interesting ideas and can help you get started quicker too. Learn quicker together 😉

Finally, here is a proof I have written, which is currently a WIP PR, as I hope to prove multiplication formulas for it as well. I proved this in my first week of doing Lean :)

Project: https://github.com/grhkm21/lean/blob/master/src/bernoulli_polynomials.lean
Zulip Chat (main collab space): https://leanprover.zulipchat.com/
Lean website: https://leanprover-community.github.io/

Finally finally, there is an ongoing project to port the current mathlib from lean 3 to lean 4, which is a new release in progress. It would be tremendously helpful to have more people to join!

#lean #leanprover #mathlib #math #maths #numbertheory

This month in mathlib (Oct and Nov 2022). https://leanprover-community.github.io/blog/posts/this-month-in-mathlib-oct-and-nov-2022/ #ITP #LeanProver #MathLib #Math

@eigenfoo
I just learned about #leanprover :
https://leanprover.github.io/

#mathlib is especially cool:
https://leanprover-community.github.io/mathlib_docs/index.html