Hello! from Ian

Stream: new members

[Ian Riley]

Hey everyone! My name is Ian Riley. I'm a PhD candidate and Faculty Instructor of Computer Science at the University of Tulsa in Tulsa, Oklahoma. I briefly used Lean 3 for a publication a few years ago but the work went in a different direction. I'm currently revisiting Lean 3/4 as a part of my dissertation effort. I intend to use Lean for Game Theory, Math, Statistics, and Logical Verification of Computer Systems (particularly self-adaptive systems) using such propositional logic as Hoare logic, temporal logical, metric temporal logic, and alternating-time temporal logic. It's been really fun getting to dive back into it especially with Lean 4. I do have some questions about Lean where ever the appropriate place might be to ask them. Otherwise, I just wanted to express my appreciation for the Lean community. It's really awesome to see that the community is still going very strong :)

[Anne Baanen]

Ian Riley said:

I do have some questions about Lean where ever the appropriate place might be to ask them.

This is the perfect place, please go ahead! You can reply in this thread for your questions or make a new thread in the #new members stream.

Are you already subscribed to the #Program verification stream?

[Ian Riley]

Hey @Anne Baanen. I just subscribed! Thank you so much. My questions are as follows (a) Is there an interpreter for lean that could be used to execute lean 4 files without a lakefile? My understanding is that's what the lean tool does, but I've encountered the "download component lean" after trying to run lean files in a lake init project and I don't know what causes that to occur?, (b) what is generally considered the state of lean 4 and is theorem proving in lean 4 as well or more developed than lean 3, (c) is there a generally held style guide for lean 4? I've been curious if there are conventions on when to use named hypotheses vs french quotes, explicit And.intro vs the constructor notation or And.right vs hpq.right, lambda vs fun to introduce variables, and tactics vs structured terms that use essentially ch.3 and 4 vs 5 of the Theorem Proving book. I checked the style guide for Lean 3 but that didn't seem to cover everything.

[Anne Baanen]

For (a): the "download component" message is generated by the elan version manager, which tries to determine which version of lean is suitable for the file, and will download and install missing versions seamlessly. This is important because Lean is not very backwards compatible. It's very similar to rustup if you happen to know that program (which it is in fact a fork of!) Generally elan needs a Lakefile or leanpkg.toml file to do its work succesfully, so I don't know if there's a good way to run random files without that information.

[Anne Baanen]

For (b): Lean 4 is already the best option for programming and simple proofs. Mathlib is currently being ported to Lean 4 so you might need to stay with Lean 3 if you heavily depend on proofs in mathlib that haven't been ported yet. There's also automatically generated mathbin files that should allow you to import mathlib from Lean 4 but I have not used those and can't say how well they work in practice.

[Anne Baanen]

For (c): I understand there are still some style issues being worked out. If we stay with mathlib's Lean 3 style, then generally I'd say:

• named hypotheses over french quotes
• constructor notation over constructor names

I believe the plan is now to use fun in Lean 4 but with a unicode \mapsto symbol instead of =>.

And finally mathlib leans somewhat to tactics but either way is acceptable. Most of the structured proof steps are also available as tactics which makes staying in tactic mode easiest.

[Ian Riley]

I typed out a reply, but it doesn't seem to have posted. I just wanted to say thank you for all of the helpful feedback. I also use rust extensively, and it's very cool that elan is a fork of rustup. I use Obsidian as a knowledge management tool. There is an execute-code plugin that can execute code snippets within markdown. I'm looking at adding lean support. I think it would be really cool to have lean proofs alongside my markdown notes. I also wanted to ask if tactics are "slower" (performance-wise) or have a larger memory footprint than equivalent structured proof steps? My guess is that the difference is negligible but wanted to ask anyway. For example, would the tactic cases with a disjunction be less performant that using the Or.elim with two lambda binder functions?