Talk:Lean (proof assistant)

Remove paragraph on features that differentiate lean?

As far as I can tell, none of these features are unique to lean:

• Compilation to javascript: Coq and F* both have this
• Native support for unicode symbols: Coq has this
• Typing symbols with LaTeX notations: this is an Emacs feature
• Own language for meta-programming: F* has this too

I think this paragraph could just be removed? 2603:400A:0:82C:FFF0:9101:2D27:7223 (talk) 00:52, 14 December 2020 (UTC)

Examples in Lean 4

As of October 2023, the examples section is in Lean 3, which the current version is not backwards-compatible with. We can borrow examples from the community's Mathematics in Lean book (which uses Lean 4 and Mathlib), to make this section of the article reflect the language's current syntax and features.

I think this is what each example should generally look like:

1. The full text of the proof, in Latex/markdown. Should be readable to anyone familiar with math.
2. The proof translated into Lean 4 code, with an explanation of what each "tactic" is doing, in comments. Tactics are basically functions built into Mathlib or core Lean that allow the language to understand steps in the proof. The most common one is "rw".
3. The output of the code. This could also be a comment.

Lean is not a theorem prover. It does not "fill in the gaps" for you or generate a proof on its own. Rather, it is a proof assistant, meaning that you can take a draft of a proof, code it, and see that it is true. This the key idea that we want readers to take away from this section.

There should also be an explanation of what Tactics are, either in the Example or Overview sections.

RedrickSchu (talk) 15:03, 1 November 2023 (UTC)