Lean & Mathlib feel consistent/coherent to mathematicians?

Stream: new members

[Dan Grigsby]

Experienced mathematicians: I’m wondering if Lean and Mathlib feel consistent and coherent to you.

I’m trying to evaluate how much of the wrangling I do with syntax and overall feel comes as a result of me, as a programmer, having less mathematical maturity.

As an example, after working with Obtain a bit, it makes sense to me why the syntax is different for AND and OR. The obtain ⟨h1, h2⟩ := h and obtain hx | hy := h syntax (more closely) fits the way a mathematician would hand write those operations. As a programmer, it initially felt inconsistent, but now I see the logic. I’m wondering how much this holds true more broadly.

There are other examples, for example the use of ·, that I /think/ are language syntax and not part of the signature of a particular lemma, but which feel inscrutable.

I’m enjoying Lean. It’s very satisfying when I complete a proof. I’m just calibrating. Thanks!

[llllvvuu]

In the case of obtain, those syntaxes actually do different things. One gives you two hypotheses and one goal. The other gives you two goals, each with one hypothesis.

[Mark Fischer]

I'm very new to all of this too and my background is much more compsci than math. So perhaps my answer won't be too enlightening.

I find a lot of the term level language feels like programming to me. Function definitions, dot syntax, destructuring/pattern matching, product & sum data types, lambda expressions. These have been around in Haskell since before I was born. They're commonplace in functional languages, but they're out in force elsewhere too like TypeScript and Rust.

Rust uses the same syntax for structs and enums, but if you look at most other languages with sum types/varients you'll often see them expressed with |. Look at F#, OCaml, PureScript, Elm, Haskell, etc.

In a way it makes sense that to pattern match on a sum type you use the pattern as when you created it. Though it only makes sense when you have a proof state that can be split by the pattern. You'll see it in an rcases pattern but not a match pattern because rcases can handle it by creating multiple goals.

---

use of ·

I don't think that's a math thing, I think that's a Lean-specific feature. It creates a λ-term for you.

def incr_a := λx ↦ x + 1
def incr_b := (· + 1)

#eval incr_a 5 -- eval to 6
#eval incr_b 5  -- eval to 6 also

-- actually, they're the same by definition since · is just syntactic sugar
example: incr_a = incr_b := rfl

Haskell lets you do the same : (+1) and so does PureScript (_ + 1). Though the syntax is a bit different and Lean's version is more powerful as it can be used a bit more freely instead of just with operators.

[Junyan Xu]

⟨h1, h2⟩ := h and obtain hx | hy := h

Some low-level type theory stuff going on here: , separates multiple arguments in the same constructor of an inductive type, | separates different constructors of an inductive type.

[Preeyan Parmar]

Using . to create lambdas is very close to what I’d say as a mathematician, eg “consider the function f(. + c)”

The syntax “\lambda x . t” or “fun x => t” I’ve always found a bit strange as a mathematician; I’d more naturally write something like “x => t”. (This is how you create lambdas in C#!)

[Junyan Xu]

It's a pity that " f(. + c)" doesn't actually work; you need (f <| . + c) for that which an untrained mathematician can't parse.

[Mario Carneiro]

f (· + c) does work, but it's not clear from this context if that's what you want - it passes fun x => x + c as an argument to f. If you want to compose the two functions you could do f ∘ (· + c).

[Jireh Loreaux]

Yeah, but with composition it's no longer reducible defeq to the other one.