lean4-raytracer VS mathlib4

Lean is currently moving to the 4th iteration which is the first intended to be a general-purpose programming language. It "is currently being released as milestone releases towards a first stable release". For now the main goal is to port mathlib to the new version, and then they will concentrate on the compiler. So it is not production ready. But that doesn't mean it is not suitable for building any programs now. There is a simple raytracer written in Lean [1]. I have built a chip8 interpreter with it and the only problem was the lack of an ecosystem, meaning I had to build the necessary libraries myself.

Now it has a RC GC and boxes everything >= 64 bits, and as the compiler isn't polished it is probably significantly slower. In the referenced raytracer repo you can find rendering time compared to the C implementation (Lean is 25x slower, but that was a year ago).

[1] https://github.com/kmill/lean4-raytracer

We essentially implemented this matrix version in Lean/mathlib to both compute the fibonacci number and generate an efficient proof for the calculation.

https://github.com/leanprover-community/mathlib4/blob/master...

In practice this isn't very useful (the definition of Nat.fib unfolds quick enough and concrete large fibonacci numbers don't often appear in proofs) but still it shaves a bit of time off the calculation and the proof verification.

As an aside, there are a number of Turing machines defined in Lean's mathlib. https://github.com/leanprover-community/mathlib4/blob/2c3ee3...

Thanks,

and there is Subobject, which looks like the subobject classifier.

https://github.com/leanprover-community/mathlib4/blob/master...

I just wonder if there are any irl meetups of people involved with formalizing mathematics, I thought that it would be a cool hobby to pick up (with some background in math and programming) but the existing libraries, like MathLib, TypeTopology or UniMath look a bit intimidating...

What is a good proof in either unimath or mathlib4 or somewhere else to get started with formal proofs? Like some well known result without too many dependencies, but still nothing trivial like propositional logic?

For searching using search terms for theorems in mathlib, there is the mathlib documentation page (for Lean 3 https://leanprover-community.github.io/mathlib_docs/ and Lean 4 https://leanprover-community.github.io/mathlib4_docs/). To find theorems by type, I find the best way is to use the `library_search` tactic from inside Lean itself.

Hello, I'd like to start learning Lean 4. I'm already reading the book, but I'm really curious to study real-life parallel. So I looked into mathlib4, but there seem to be a lot of dependencies between the the files. So I wonder the following: