Where are you writing Lean in public? (share GitHub links)

Stream: general

[Simon DeDeo]

We (myself and Balint Gyevnar, a postdoc at CMU) are doing some studies of how people write Lean code — in particular, how a project develops over time, how code gets filled out, how errors get found, and so on. Among other things, we're interested in how AI systems might try to make sense of what you're doing, in ways parallel, or oblique, to your own journey.

We would be very grateful if people would be willing to share links to Github repos where they've been writing code. Ideally, these would be

(1) smaller personal projects, so we can see how individuals or small groups develop ideas over time, potentially in a playful or self-teaching mode.

(2) projects where at least some of the code is, indeed, finished — a theorem is proved, definitions are constructed and probed — so that we can get a sense of where the project was (at least by the end) intended to go.

(3) things you think are particularly interesting or creative — even if the project didn't reach the ultimate desired form.

We do not need super-proficient Lean gurus! — beginners and hobbyists would be lovely. For example, Iif you're teaching a course where students are keeping their projects in a Github, this could be ideal, or if you were using Lean for something adventurous as a passion project. Right now we're not sure how to handle larger projects where there are pull requests, administrators, and so on, but we're hoping eventually to scale up to big things like mathlib.

If you're willing to share, the only thing we need is that the Github project be set to "public" so that we can see it (otherwise we'd need to get ethics clearance.)

Please share them here, or if you like, by e-mail to sdedeo[at]andrew.cmu.edu ; and please don't be shy.

[Alok Singh]

https://github.com/alok/Limestone

[Yaël Dillies]

I think this is a very good idea! Here are mine: https://github.com/YaelDillies/LeanAPAP, https://github.com/YaelDillies/LeanCamCombi, https://github.com/YaelDillies/Toric

[Snir Broshi]

There's the projects page on the community website and links from 100.yaml and 1000.yaml, they contain 31 repos that aren't under leanprover-community or leanprover. There are also a lot of repos already shared on Zulip. Do these not fit? I think most of them are personal projects with a specific goal

[Arthur Paulino]

https://github.com/argumentcomputer/ix is a (WIP) zk-kernel for content-addressed Lean declarations (definitions, theorems etc).

[Kevin Buzzard]

https://github.com/kbuzzard/ClassFieldTheory (me and Richard Hill and several PhD students), https://github.com/ImperialCollegeLondon/FLT (one year into a project initially trying to reduce FLT to the 1980s).

You know about https://reservoir.lean-lang.org/ right?

[Simon DeDeo]

These are all lovely — thank you! We will keep scanning Zulip for GitHub projects.

One challenge is that people often create a "fresh" github before showing their work to others on Zulip, so we lose a lot of the early brainstorming/error making/blind alley data. The fantasy data is when we can see the lean files go from nearly empty and full of sorr[y/ows] to completion. If people want to share their more secret ones, we'd be delighted!

One exception we've found so far are things like Tao's group projects https://github.com/teorth/pfr

[Dagur Asgeirsson]

https://github.com/dagurtomas/LeanCondensed contains some WIP code on various results in condensed mathematics, right now mostly related to solid abelian groups, but not with a single end goal

[Eric Paul]

https://github.com/ericluap/OrderedSemigroups (a finished project on ordered semigroups)
https://github.com/ericluap/AutLinOrd (an ongoing project on automorphisms of linear orders)

[Pim Otte]

https://github.com/pimotte/TutteLean has a decentish history of my formalization of Tutte's theorem. The fully refactored version is what ended up in Mathlib, so that's not contained in this repository, but the code is in these PRs. Feel free to ping me if you have any follow-up questions:)

[Jon Eugster]

https://github.com/hhu-adam/lean-i18n - a fully functional, yet not feature complete i18n package.
https://github.com/leanprover-community/lean4game/tree/main/server - the Lean package here is under a subdirectory server

[Chris Birkbeck]

https://github.com/CBirkbeck/LeanModularForms has a bunch of modular form stuff that is being slowly PRd to mathlib. There is also https://github.com/thefundamentaltheor3m/Sphere-Packing-Lean where the Sphere packing project is happening.

[Martin Dvořák]

Below I'm sharing a mix of personal projects of various sizes, from 70 lines up to 15k lines. I omitted larger collaborative projects, as they are usually based on pull requests.

Chomsky hierarchy in Lean 3:
https://github.com/madvorak/grammars

Its WIP port to Lean 4:
https://github.com/madvorak/chomsky

[everything that follows is also in Lean 4]

Left-behind attempt to create a library about Semi-Thue systems (a.k.a. string rewriting systems):
https://github.com/madvorak/thue

Left-behind attempt to create a library about fractional operations:
https://github.com/madvorak/fractional

Koch 2D snowflake generator for 4D Golf (just a little script, no proofs):
https://github.com/madvorak/lean4-koch

Duality theory in linear optimization and its extensions:
https://github.com/madvorak/duality

General-Valued Constraint Satisfaction Problems:
https://github.com/madvorak/vcsp

A few teaching repositories:
https://github.com/madvorak/lean-mam
https://github.com/madvorak/lean4-course
https://github.com/madvorak/fecssk
https://github.com/madvorak/lean4-tutorial
https://github.com/madvorak/formalisms

[GasStationManager]

Here's one from me, still (slowly) making progress. One thing that is a bit unusual is that the explicit goal is for most of the Lean code to be written by AIs.

https://github.com/GasStationManager/ArtificialAlgorithms

[Vasily Ilin]

We have many projects in our UW Math AI Lab: https://github.com/uw-math-ai

[Paul Schwahn]

https://github.com/PSchwahn/IncidenceGeometry/

[François G. Dorais]

Mature projects:

• https://github.com/fgdorais/lean4-unicode-basic
• https://github.com/fgdorais/lean4-parser

Experimental projects:

• https://github.com/fgdorais/lean4-ascii
• https://github.com/fgdorais/lean4-unicode-lemmas
• https://github.com/fgdorais/lean4-automata
• https://github.com/fgdorais/algebra4
• https://github.com/fgdorais/logic4
• https://github.com/fgdorais/extra4

A few more projects in the dust bin...

[Kim Morrison]

You're scraping every branch of every fork of Mathlib, right? There's a lot there.

[Oliver Butterley]

Here's our project for formal verification of Rust code for elliptic curve cryptography: https://github.com/Beneficial-AI-Foundation/curve25519-dalek-lean-verify

Workflow, slightly differently to many maths projects, is: Step 1: extract Rust to Lean, Step 2: write spec theorems in Lean, Step 3: prove those spec theorems.

[Malvin Gattinger]

https://github.com/m4lvin/lean4-pdl

[Roman Bacik]

https://github.com/roman3017/FinLin