sorry

Stream: mathlib4

[Alexander Bentkamp]

Hello @Mario Carneiro @Gabriel Ebner @Kevin Buzzard ! Would you be ok with contributions to the mathlib4 repo that contain sorrys? I think it would help experimenting with Lean4 if more lemmas were available, no matter if they are actually proven or not. I've already started my own copy of mathlib4 with lots of sorrys for just this purpose and I'd be happy to merge it into your mathlib4 repo.

[Mario Carneiro]

Hm, I'd prefer not to, but if you like you can post the sorries and I can fill them in :)

[Alexander Bentkamp]

Sounds like a good deal :D

[Jannis Limperg]

For experimentation purposes, you could also look at the various automatic porting tools. Afaik they can already port the vast majority of mathlib definitions (but not the proofs), so you can get all the mathlib lemma statements.

[Julian Berman]

So autoporting tools give you sorried autoported lemmas. Does that make Mario the first auto-proving tool?

[Kevin Buzzard]

I have plenty of non-master branches with sorrys

[Mario Carneiro]

The auto-porting tools will port full proofs, but only as low level proof terms, not as tactic scripts suitable for insertion into a lean file

[Alexander Bentkamp]

Ok, but I could use mathlib definitions and theorems in a Lean4 project in this way, right? I'll try it out.

[Gabriel Ebner]

Yes, the mathport tool generates Lean 4 olean files from current mathlib:
https://github.com/dselsam/mathport/ (EDIT: I'm bad at copy&paste)
You can import them in Lean 4 and it seems to work reasonably well, but there's a bit of impedance mismatch of course with different type-classes etc.

[Gabriel Ebner]

@Aurélien Saue has been working on turning these olean files into Lean 4 source files (which don't compile yet). This is not as trivial as it sounds, because the olean files contain all kinds of auto-generated definitions that need to be reverse-engineered. You can see an example of its current output here:
https://github.com/AurelienSaue/Mathlib4_auto/blob/master/Mathlib/dynamics/flow_auto.lean

[Alexander Bentkamp]

How do I set up the directory and toml file so that I get access to the definitions in the olean files?

[Gabriel Ebner]

I would try to follow the instructions in the README, and then hope that the examples work. https://github.com/dselsam/mathport/blob/master/Lib4/Examples/Nullstellensatz.lean

[Alexander Bentkamp]

Oh, alright! Thanks!