Lean 4.0

There's plenty of published papers about newly formalized proofs, even in "undergrad" math. A formal proof development generally brings to light new information about the original proof, both by plugging all potential inaccuracies/missing steps and in being especially easy to refactor, abstracting out common patterns that might be reused elsewhere.

I agree; for simple and "beginning intermediate" tasks, Functional Programming in Lean has it all; but the more advanced features are only documented in the source code and doc-strings. There is also a lack of general listings: for data structures, for file access API, for algorithms etc.

I'm not looking to use it as a programming language, but I'd like to see an introduction to theorem proving using Lean that is more explicit in its explanation of semantics than the ones that assume an existing math background

I don’t think that your post is hostile. But from what I’ve heard, it is untrue because Lean 4 is intended to be a general purpose programming language, not only a theorem prover. I can’t find a source that directly states this goal but at the least this paper by Leo de Moura and Sebastian Ullrich presents it as a programming language:

https://link.springer.com/chapter/10.1007/978-3-030-79876-5_...

Microsoft also sponsored David Thrane Christiansen’s book, Functional Programming in Lean[1] (which I’m sure you know about!). That is another indication that they intend to reach programmers.

[1] https://leanprover.github.io/functional_programming_in_lean/

How can the audience of a general-purpose programming language not be "programmers"?

I think that is unnecessarily hostile; I believe Lean 4 can become a very capable programming language for mundane tasks!

I just did a recursive scrape of the tutorial site, converted the html to text, then did a word count using wc and simply divided it by the average number of words per page. Word in this case includes things like '(' and syntax characters.

Regardless it was a rough metric meant to be demonstrative of the level of effort to go through the tutorial.

The point is as an answer to the basic question "what is this and why should I care?" Responding with something over 10 pages is likely unadvisable, yet alone over 100. "Over 100" here is effectively equivalent to "over 5,000". The target should be like 0.25-5, and closer to the 0.25.

Elevator pitch it.

1. For (target customers)

2. Who are dissatisfied with (the current market alternative)

3. Lean is a (new product category)

4. That provides (key problem-solving capability).

5. Unlike (the product alternative),

6. Lean (describe the key product features).

https://www.elevatorpitchessentials.com/essays/CrossingTheCh...

Oops! I checked the spec and it's supposed do something more like this:

  def f (n : Nat) : String :=
    Option.getD
      (Option.merge String.append
        (if n % 3 = 0 then "Fizz" else none)
        (if n % 5 = 0 then "Buzz" else none))
      (toString n)

  #eval List.map (fun k => f (k + 1)) (List.range 100)

  theorem poop (n : Nat) :
      f n = "FizzBuzz" ∨ f n = "Fizz" ∨ f n = "Buzz" ∨ f n = toString n := by
    unfold f
    split <;> split
    · exact Or.inl rfl
    · exact Or.inr (Or.inl rfl)
    · exact Or.inr (Or.inr (Or.inl rfl))
    · exact Or.inr (Or.inr (Or.inr rfl))

Thank you. I must admit, I have trouble making sense of it.

Just for comparison, in Typescript you can write:

  function f(n:number){
    if (n%3==0 && n%5==0) return "FizzBuzz"
    if (n%3==0) return "Fizz"
    if (n%5==0) return "Buzz"
    return "";
  }

Then, I can write:

  function *iFizzBuzz(steps:number){
     for (let i=0; i<steps; i++){
        const fb = f(i); 
        if (fb) yield fb;
     }
  }

  const fizzBuzz100 = Array.from(iFizzBuzz(100));

Awesome! Where did the "split_ifs" tactic come from though? Mathlib? In your opinion does it make sense to do program verification without using Mathlib, or would you recommend just using it pretty much all the time?

That being said, nequo's request is not unreasonable; given Lean's advanced metaprogramming facilities, their request should be easy to implement.

The nice thing nequo's example illustrates is rank polymorphism: list comprehensions work with lists, products of two, three, four,... lists with the same easy notation : `[n-ary function | x_1 <- List_1, ..., x_n <- List_n]`. It is quite nice to have this, especially for complex numerical operations.

Note also that unlike Lean 3, in Lean 4 `List` does not inherently implement `Applicative` or `Monad`, so your code cannot work as is.

Haskell has always been a language where there are many ways to skin any particular cat, for reasons from ergonomics to expressiveness to theoretical niceness or practicality. "Learn the idioms" has nothing to do with it. Why didn't you just use do-notation instead, for example, than write some applicative mess where it isn't needed?

It's not rocket science why someone would ask this. I don't always use list comprehensions. But sometimes I do. They have open arity and the syntax doesn't as often require things like parenthesis to handle fixity conflicts between other (non-applicative) operators. They are asking about list comprehensions, just because they think it's nice. It is a very simple question and talking about applicative is irrelevant.

That's perfectly fine Haskell, but I wouldn't say that using Applicative is much of a Lean idiom. Especially in the mathlib, people prefer using custom notation that looks like math notation or using the underlying functions directly rather than by using generic point-free notations. For example, you'll see `⨆ i, s i` for a supremum across the values of `s`, vs a point-free version.

Thanks,

and there is Subobject, which looks like the subobject classifier.

https://github.com/leanprover-community/mathlib4/blob/master...

Here's a Lean 3 development of a bunch of topos theory https://github.com/b-mehta/topos/tree/master/src , but it's not in the maths library (and now needs to be updated to Lean 4, although the community have had great success with that kind of project; one million lines of mathlib was translated from Lean 3 to Lean 4 using a combination of automation and human work)