[prisonguard]

I've always thought theorem proving to be about proving equality of the function and the result.

Lean to me is not only obscure but unapproachable by someone from a non-mathematical background.

Take this snippet for instance

      theorem nat.add_comm : ∀ (n m : ℕ), n + m = m + n :=
      λ (n m : ℕ),
      nat.brec_on m
         (λ (m : ℕ) (_F : nat.below (λ (m : ℕ), ∀ (n : ℕ), n + m = m + n) m) (n : ℕ),
            nat.cases_on m
               (λ (_F : nat.below (λ (m : ℕ), ∀ (n : ℕ), n + m = m + n) 0),
                  id_rhs (n + 0 = 0 + n) (eq.symm (nat.zero_add n)))
               (λ (m : ℕ) (_F : nat.below (λ (m : ℕ), ∀ (n : ℕ), n + m = m + n) (nat.succ m)),
                  id_rhs (n + (m + 1) = nat.succ m + n) (eq.symm (nat.succ_add m n) ▸ congr_arg nat.succ (_F.fst.fst n)))
               _F)
         n

If we want to democratise formal methods and theorem proving, we should lean towards natural language expressions of proof and not mathematical expressions and greek characters.

This is the path that languages such as Idris https://www.idris-lang.org/ have taken

[miloignis]

That snippet is the result of printing out the internal structure of the proof, not how the proof was actually written. You'll notice that what a human actually wrote and would normally read is the code block mentioned directly above in TFA, which is much more sensible:

  lemma nat.add_comm : ∀ n m : ℕ, n + m = m + n
  | n 0     := eq.symm (nat.zero_add n)
  | n (m+1) :=
    suffices succ (n + m) = succ (m + n), from
      eq.symm (succ_add m n) ▸ this,
    congr_arg succ (add_comm n m)

Also, this example proof is explicitly about math (the commutativity of addition on natural numbers), so it's appropriate and not surprising that it uses mathematical notation.

[tsimionescu]

I don't think you have any chance of approaching formal methods if the notation is a stumbling block.

The difficulty and verbosity of formal proofs is huge even with the very concise mathematical notation. And learning the notation itself is a very small stumbling block compared to learning the actual theorems and logic that you need to use.

So while I am not a fan of mathematical notation for general programming (which is often quite un-mathematical in fact) formal proofs are a place where this notation absolutely shines. I can't even imagine how much uglier the proof above would become if you had to replace `∀ (n : ℕ)` with something like `for any natural number n`.

[prisonguard]

there has to be a better way for a beginner to learn Lean even with the faintest high school mathematics recollection.

I can still do theorem proving in Idris excluding the mathematical notation and still learn concepts such as totality, covering, equality etc

[ykonstant]

A better way than what? The snippet you posted has nothing to do with how a beginner (or intermediate) learns Lean.

[sirwhinesalot]

Forall (n: Nat)

Is perfectly reasonable.

If conciseness was that important theorem provers would have syntax like APL.

[tsimionescu]

Why is forall any less formal than ∀? Or Nat less formal than ℕ? Especially when these are symbols that most will have learned in high school?

[sirwhinesalot]

They're not on my keyboard.

[Kranar]

I sympathize with your view, I genuinely do, but to write out formal methods using natural language expressions results in quite a few problems. For one, it results in incredibly long proofs, like this simple proof written out in natural language would take up pages.

Second, it makes it harder to identify patterns. Writing things out in a formalism lets you identify syntactic patterns and employ techniques like factoring, cancelling, seeing symmetries and other purely syntactic properties. When you write things out in natural language you lose the ability to see these things clearly. Being able to see purely formal syntactic properties helps reinforce your confidence in a proof or can help you identify potential flaws in it. It's like with programming styles and conventions, one thing I tell developers is an important reason for choosing one style over another is if it makes wrong code look wrong visually.

Third, and this is just a personal matter... it results in a type of culture of writing that I find is often pretentious and full of unnecessary baggage. When I read an academic paper I cringe at how bad most writing is and try my best to skip to the formal part of the paper.

[voxl]

Something else important to note: this proof of commutativity of addition on natural numbers is definitely _not_ how you normally write these proofs in Lean.

Here is a closer approximation to how someone would actually write the proof in Lean:

  lemma add_comm (a b : ℕ) : a + b = b + a :=
  begin
    induction a with a IH,
    rw (add_zero b),
    rw (zero_add b),
    trivial,
    rw (add_succ b a),
    rw (succ_add a b),
    rw IH,
    trivial
  end

[prisonguard]

thank you for explaining, but do i need a special keyboard just to type out the natural number type?

[deadbeef57]

No, you can just type `\nat` and the Lean extension in VScode will turn it into `ℕ`. Similarly, you can type many LaTeX macros, and the will render in unicode. Examples: `\times` becomes `×` and `\to` becomes `→`, etc...

[nodogoto]

No, you just type \N. You can also use `nat` instead if you prefer.

[mcguire]

Brute force string search:

    /*@
      // There is a partial match of the needle at location loc in the
      // haystack, of length len.
      predicate partial_match_at(char *needle, char *haystack, int loc, int len) =
        \forall int i; 0 <= i < len ==> needle[i] == haystack[loc + i];
     */

    /*@
      // There is a complete match of the needle at location loc in the
      // haystack.
      predicate match_at(char *needle, int n, char *haystack, int h, int loc) =
        \valid(needle + (0 .. n-1)) && 0 <= n < INT_MAX &&
        \valid(haystack + (0 .. h-1)) && 0 <= h < INT_MAX &&
        n <= h && loc <= h - n &&
        partial_match_at(needle, haystack, loc, n);
     */

    /*@
     requires \valid(needle + (0 .. n-1)) && 0 <= n < INT_MAX;
     requires \valid(haystack + (0 .. h-1)) && 0 <= h < INT_MAX;
     requires n <= h;
     assigns \nothing;
     ensures -1 <= \result <= (h-n);
     behavior success:
        ensures \result >= 0 ==> match_at(needle, n, haystack, h, \result);
     behavior failure:
        ensures \result == -1 ==>
          \forall int i; 0 <= i < h ==>
            !match_at(needle, n, haystack, h, i);
     */
    int
    brute_force (char *needle, int n, char *haystack, int h)
    {
      int i, j;
    
      /*@
        loop assigns i, j;
        loop invariant 0 <= i <= (h-n) + 1;
        loop invariant \forall int k; 0 <= k < i ==>
          !match_at(needle, n, haystack, h, k);
       */
      for (i = 0; i <= h - n; ++i) {
        /*@
          loop assigns j;
          loop invariant 0 <= j <= n;
          loop invariant partial_match_at(needle, haystack, i, j);
        */
        for (j = 0; j < n && needle[j] == haystack[j + i]; ++j);
        if (j >= n) {
          return i;
        }
      }
      return -1;
    }

[ratmice]

One thing which perhaps is not captured well in the article, is that rather unlike when reading/writing source code, where stepping through lines of code is a relatively uncommon task only done debugging. For interactive theorem provers it is a given. He discusses the bottom up & top-down approach to the solving goals with tactics & otherwise, but typically in both cases you will be stepping through expressions to get a better understanding. They generally aren't written to be read from just the source text alone.

[nh23423fefe]

> if we

Who is this we? The people who understand mashed with the ignorant who put in no work?

> to democratise

So that those in the know can be further diluted with dabblers who contribute nothing and complain about their ignorance?

[flir]

raises hand I'd like more tools that involve me putting in no work, please. They help me achieve my real-world goal faster.

[prisonguard]

making thing obscure and less obvious is anti-intellectual, its getting harder and harder for new developers to gain a footing in software development

also why tools like chatGPT have gained so much popularity

[nh23423fefe]

3 assertions with no implications

[UncleEntity]

Yep, like the olden days where the only people “in the know” knew Latin. Or, before that, Greek.

Then someone had to come along and invent the printing press.

[Joker_vD]

> Or, before that, Greek.

Greek (or koine, for that matter) was pretty much street vernacular in the Roman/Byzantine empire during that period you're likely talking about.

[nodogoto]

> Lean to me is not only obscure but unapproachable by someone from a non-mathematical background. ... If we want to democratise formal methods and theorem proving ...

For whom is that a goal? Are there really that many individuals at the intersection of "I need to use a theorem prover" and "I don't have formal mathematical training"?