Abhishek Chugh

Stream: new members

[Abhishek Chugh]

Hello! I am new to Lean. Excited to be part of this community.
I am most intrigued by Lean's ability to (relatively) easily generate computer verified and fully transparent proofs.
I am interested in making these proofs available to the broader math community.

[Abhishek Chugh]

Noob question: What would be the quickest way to unwrap a Lean proof into a tree/graph of steps (till I reach axioms & definitions) into a nice data structure? The data structure can be in any programming language (like C/Python/Java etc)

For example: How to get the actual complete proof friendship theorem (without tactics):
https://github.com/leanprover-community/mathlib/blob/2688d42b3e1b8f65a48e5cfc77f6db3c11e00ccf/archive/100-theorems-list/83_friendship_graphs.lean

[Johan Commelin]

I guess you'll want to take a look at leancrawler

[Johan Commelin]

Also see https://github.com/leanprover-community/lean-client-python

[Abhishek Chugh]

Thanks for the pointers. I will look into this now.
Also, I am guessing it is easy to unwrap the lean files into some format that can be verified independently. is there a tool/command to do this?

[Johan Commelin]

There used to be an independent verifier, but I'm not sure if it is still compatible with the latest community version of Lean. It probably is.

[Abhishek Chugh]

I see. Thanks Johan.

[Rob Lewis]

Johan Commelin said:

There used to be an independent verifier, but I'm not sure if it is still compatible with the latest community version of Lean. It probably is.

It is (at least, leanchecker is). It runs every time you push anything to mathlib! https://github.com/leanprover-community/mathlib/blob/master/.github/workflows/build.yml#L139

[Rob Lewis]

The export format is explained here

[Abhishek Chugh]

Thanks Rob. I am intereseted in creating a graph of theorems/lemmas of all proofs in Lean. I am guessing it should be possible to get it from this format.

[Rob Lewis]

You're probably more interested in leancrawler then. https://github.com/leanprover-community/leancrawler

[Reid Barton]

I don't think the export format distinguishes definitions (in the sense of Lean's def) from lemmas, but otherwise it should have the information you need

[Rob Lewis]

I think @Patrick Massot has some recent changes to leancrawler, or were those for mathlibtools?

[Reid Barton]

But leancrawler will give you more information like def/lemma, position information, human-readable types

[Abhishek Chugh]

Hmmm...leancrawler is what I need then. I want to make it available to the average mathematician - so information that aids human- readablity is important.

[Patrick Massot]

I have local changes to leancrawler on my home computer that I should try to push tonight. But I don't think this will help to "generate computer verified and fully transparent proofs". Maybe you're asking two independent questions?

[Yury G. Kudryashov]

May be, the goal is to generate something that a human can read/browse from a computer verified proof. Note that most probably it won't be really readable: many tactics generate unreadable proof trees.

[Yury G. Kudryashov]

If you want to understand how the proof works, the original (most probably, tactic mode) proof is your friend.

[Abhishek Chugh]

@Patrick Massot @Yury G. Kudryashov sorry I missed your messages
I have also come to understand that the tactics are going to be far more readable than the fully unwrapped proofs - so I think it would be best to have all the lemmas along with the tactic-based proof shown to the user.