Lean outside of academia

Stream: new members

[Dan Abramov]

I'm curious to hear from folks who are learning Lean outside of academia. How did you come about it? What are you learning it for? Does anyone pay you to do it, or is it for fun?

Not 100% sure if these types of broad questions are on-topic, pardon if not!

Personally I'm learning it "for fun". I know a lot of people with academic background are learning it because it's relevant to their research, which makes sense. But I'm curious to hear more from "outliers", like what's drawing you in, do you hope to do it more "seriously", etc.

Thanks!

[Weiyi Wang]

I am a math enthusiast learning it for fun. I do software engineering for job, and I was intrigued when I learned math can also be done on a computer like programming (and has already grown into a large library). I hope I can do it more seriously, though I still struggle reading a lot of high level stuff, lean code or math itself, so there is still a long way to go

[suhr]

Hello! As a curious programmer I know a lot of cool computer things. Lean is not the first language with dependent types I learned (and I heard about dependent types long long ago), but my familiarity with dependent types was surface-level before I dived deeper.

I also like cool math and want it to be more accessible. So I hope to continue writing my book (I wish I had more time for it).

[Arthur Paulino]

I first tried Rocq but, being a programmer, I really disliked the syntax. Then I tried Lean and it made a lot of sense to me.

At first, I just wanted to understand this "math via types" thing a colleague I had in college was doing. But the community was transitioning from Lean 3 to Lean 4 and I got to enjoy it as a powerful programming language.

Nowadays I am paid to program in Lean and Rust, my two preferred languages. We're developing ix.

[suhr]

Heh, a fellow Rust programmer.

[Weiyi Wang]

Oh, I also came from Rust

[Weiyi Wang]

:rolling_on_the_floor_laughing: There must be a secret Rust->Lean pipeline

[suhr]

@ralfj said that Rust programmers already know separation logic. So it makes sense that I now occasionally contribute to iris-lean...

[Julian Berman]

I'm definitely in the "fun rather than for work or research" bucket as well. I initially encountered Lean (like many did) from a video Kevin did a few years ago (actually 5 years ago now!). My interests have mostly revolved around "hm, I think I'm a good programmer, and I did undergrad math 10+ years ago, that means I can parlay my programming skills back to learn more math via Lean, right? Right??" (spoiler: mm not so much. Or it's still quite a challenge!) I'd say I've have nearly no interest in it as a programming language as opposed to theorem proving which I'd never encountered elsewhere in my years in the software ecosystem(s). It's still just as fun as always to hang around Everest base camp and every so often try to meander up a path.

[aron]

I'm a software engineer and I've been intrigued by dependent types for a while – but I really got into it when I wanted to experiment with more exotic type systems. Especially when I started to get serious about trying to implement type systems myself. I'm still working on implementing and proving some properties of simpler type systems first. But once that's done I'm hoping to move on to implementing some of my own type system ideas I've had

[Christian Krause]

I'm a high school student with some programming experience (rust :crab:) and I wanted to get a bit into math (by formaliting banach tarski in lean). At first i thought "I know programming, lean can't be that different/difficult" (Spoiler: it was). But in the following two years I learnt a lot about math (especially that i dont know anything) and I enjoy using lean very much. You could say that lean lead me to the decision to study math and physics next winter semester :tada:.

[Aaron Liu]

I'm a high school student that got into Lean through Haskell, and I had very much fun with it as a game, using it to improve my proof writing. Then I found out I could learn math by reading mathlib, and that was fun too, and I learned a lot. Then I got interested in metaprogramming, so I learned that too. Lean is so much fun!

[Christopher Hoskin]

I went into doing IT for academia after I finished my doctorate (in 2004) - partly because it gave me a way to continue dabbling in mathematics in my spare time. In the early years I managed to co-author a couple of peer reviewed papers, but more recently there hasn't been anyone I check my work with and I haven't got the several weeks of contiguous time it would take me to assemble my notes into a paper. I've always been a fan of LaTeX for typesetting, but also been disappointed that it has no understanding of what I'm writing and will quite happily beautifully typeset complete nonsense.

I spent about three years trying to get into Isabelle. I'm usually quite happy as an autodidactic, but the learning curve was just too steep, and the documentation required a deeper knowledge of both computer science and mathematical philosophy than I had as a practitioner of IT and maths.

Then during a sleepless night during the pandemic I started watching the "Lean for the Curious Mathematician" videos on you tube and started playing the natural numbers game and found that this was a learning curve I could manage. Mathlib's GitHub PR-based approach to also worked much better for me than trying to write papers.

For me the attractions of Lean / Mathlib are:

• An independent check that I've not made a silly mathematical mistake
• A better structured way of organising my ideas than writing in notebooks (by now I have about 20 a4-sized handwritten notebooks, with almost no indexing...)
• Easier for a time-constrained person to make small, incremental improvements to a shared body of knowledge over several years

One unexpected benefit has been that it's caused me to learn about all sorts of mathematical ideas which I hadn't previously been exposed to (lattice ordered groups for example).

[Yaël Dillies]

Thanks Christopher for all this insider information! I assume I have reviewed most of your PRs to mathlib, yet I never knew how you got there

[Violeta Hernández]

I found Lean through a friend back in a 2021 (who funnily enough also introduced me to Rust). I found a contribution niche within Mathlib and I've happily stuck to it since.

[Christopher Hoskin]

Yaël Dillies said:

Thanks Christopher for all this insider information! I assume I have reviewed most of your PRs to mathlib, yet I never knew how you got there

And I'm very grateful for all the hours of review that you and @Eric Wieser in particular have given me!

[Rado Kirov]

I've always liked math and programming. I was trained as mathematician but flunked out of academia after the first post-doc. Luckily, I knew enough programming to get a software eng job and have been doing that for the last 15 years. Playing with Lean gives me a good opportunity to reconnect with the math world that I have left behind (but still have feeling towards), while bringing some of my more recent software experience. Basically, it offers me an integration of the two main things I have spend many hours of my life working on.

Also, I like playing logic puzzle games, and writing proofs in Lean, tickles my brain the same way as doing logic puzzles, much more than doing the same on pen-and-paper. So not in a particular rush to do "serious" instead of "unserious" things with it.

Does anyone pay you to do it, or is it for fun?

All fun. If there was money in math, I might have stuck around longer :) . Curious about your experience with real-world engineering, but from what I have seen working in FAANGs (which is writing code in service of making money) they don't need provably correct software (some caveats in cryptography etc), because that software interacts with the real world and one can't even define "correct" to prove it so.

[metakuntyyy]

I think one day I stumbled upon a metamath proof and I was blown away that I could browse every proof and every inference down to its definitions and axioms. I think I had the vague idea that formal proofs exist but I didn't know that everything could be explained down to the axioms. That day was very fun as I browsed how certain mathematical theorems/definitions are presented formally. I usually just yoink the proofs here to port them to metamath. However a few ago I started to be way more serious with lean and started digging into the system way deeper.

The fun thing is is that I learned so much through the side project formalisation. One notable fact, that I previously never even registered is that the universal property of quotients is way nicer than I thought. In prosa it's described as the triangle commutes, which is an unfortunate description as it hides the most important property which is an equality. In general I learned that equality does not get the respect that it deserves. Using metamath/lean made me aware how often we unconsciously use equality.