Zulip Chat Archive

Stream: new members

Topic: Trees


Callum August (Oct 05 2020 at 15:16):

Hello, I was wondering if anyone knows of any work on trees in Lean? I have looked at rbtree and mathlib tree.

Johan Commelin (Oct 05 2020 at 15:49):

Do you mean tree as in graph theory, or as in data structure?

Johan Commelin (Oct 05 2020 at 15:49):

I think there is theoretical overlap, but probably not much practical overlap

Callum August (Oct 05 2020 at 16:00):

As in the data structure

Adam Topaz (Oct 05 2020 at 16:33):

I don't really know much about this, and I don't really know what tree means, but I was under the impression that W-types subsume all possible definitions of tree.

Adam Topaz (Oct 05 2020 at 16:34):

src#W

Christopher Iliffe Sprague (Feb 27 2021 at 17:18):

Hi! I am new to Lean. My closest related experience is with Mathematica.
I am working on a special problem, and I am not sure whether I should use Mathematica or Lean.
I have a family of sets that are indexed by an ordered tree, and their relations between eachother depends on their indexing.
I need to prove that some of these sets are disjoint.
Should I stick with Mathematica or use Lean for this?

Kevin Buzzard (Feb 27 2021 at 17:30):

can you prove anything with Mathematica? What do you mean by prove?

Christopher Iliffe Sprague (Feb 27 2021 at 18:09):

Kevin Buzzard said:

can you prove anything with Mathematica? What do you mean by prove?

Thanks for your response! From what I've read you can use first-order logic to prove some thing like this: https://reference.wolfram.com/language/ref/FindEquationalProof.html.
By "prove", I mean state a theorem and prove it with a set of lemmas. Forgive me if I am not using the correct parlance.
From further reading, it seem Lean can do pretty much anything. So, now my question is: could I transfer what I produce in Lean to human-readable math in latex?

Kevin Buzzard (Feb 27 2021 at 18:10):

Oh, I didn't know Mathematica could do proofs like that -- that's why I was confused.

Christopher Iliffe Sprague (Feb 27 2021 at 18:15):

Kevin Buzzard said:

Oh, I didn't know Mathematica could do proofs like that -- that's why I was confused.

Could you give me a recommendation on where to start for coding ordered trees and families of sets (in Euclidan space) that are indexed by such a tree?

Bryan Gin-ge Chen (Feb 27 2021 at 18:26):

We have a page of learning resources here. I recommend working through the Natural Number Game and some of the other tutorials to see what it's like to use Lean.

Huỳnh Trần Khanh (Feb 28 2021 at 14:42):

could I transfer what I produce in Lean to human-readable math in latex?

I'm afraid you have to do that manually—currently there are no usable tools and Lean proofs are not intended to be read outside of a Lean-aware text editor. Tactics can mutate the context and the mutations can be pretty hard to trace without the infoview, which is the right pane in Visual Studio Code with the Lean extension and the Lean web interface.


Last updated: Dec 20 2023 at 11:08 UTC