Let me take a random example, in a random recent commit in mathlib:
lemma inverse {f : γ → β} {g : β → γ}
(hf : is_linear_map f) (h₁ : left_inverse g f) (h₂ : right_inverse g f): is_linear_map g := +⟨assume x y,
have g (f (g (x + y))) = g (f (g x + g y)),
by rw [h₂ (x + y), hf.add, h₂ x, h₂ y],
by rwa [h₁ (g (x + y)), h₁ (g x + g y)] at this, +assume a b,
have g (f (g (a • b))) = g (f (a • g b)),
by rw [h₂ (a • b), hf.smul, h₂ b],
by rwa [h₁ (g (a • b)), h₁ (a • g b)] at this ⟩ +
Mario Carneiro
@digama0
In isabelle all those would be one-liners I'm sure
there's not much going on except the have lines
sgouezel
@sgouezel
What is going on is essentially clear, but nowhere is it explicitely said that you are proving that g(x+y) = g x + g y, or that g(a . b) = a.g b, while this is the central point for a linear algebra newbie.
Patrick Massot
@PatrickMassot
Isn't clear from the have lines?
sgouezel
@sgouezel
It would read like that in Isabelle:
have g (f (g (x + y))) = g (f (g x + g y)) by (simp add...)
Mario Carneiro
@digama0
You have show ?thesis at the ends of your proofs though
sgouezel
@sgouezel
then show g(x+y) = g x + g y by (simp add...)
and then the same with g(a.b) = a.g(b) said explicitely
Yes, there is show ?thesis when ?thesis is something explicit you are proving. when there are multiple goals, there is no ?thesis, and you have to say what you are doing :)
I am not saying that the proof above is not readable, in fact I think it is, but it could be made even more explicit...
Mario Carneiro
@digama0
You can always be more explicit
Patrick Massot
@PatrickMassot
To me the real question is: Mario, do you have any idea how long it will take to get good automation in Lean? Is it something in months or years?
Mario Carneiro
@digama0
Some in months, some in years
sgouezel
@sgouezel
The question is how explicit you want to be, and for sure tastes can differ. I find it funny though that in the above proof, if you don't already know in which direction you are heading, then the goal is nowhere explicit.
Patrick Massot
@PatrickMassot
Reaching the level of what we saw in Sébastien's Isabelle files would be years away then?
Kevin Buzzard
@kbuzzard
It means you can do many many things, but not everything. For instance, you can not define Q_p easily (as a field that would depend on a prime parameter p). And if you want to define the adeles, you are really into trouble.
Mario Carneiro
@digama0
No, that's primarily a matter of more theorems actually
Patrick Massot
@PatrickMassot
Or maybe we need more catchy names for tactics. I like "blast"
Mario Carneiro
@digama0
Most of the tactics aren't doing anything interesting in the readable proof either
Kevin Buzzard
@kbuzzard
I am hoping that by mid-January we have the p-adic in Lean and by Feb the adeles, and I will be focussing on these things then, as I am teaching a graduate course on this stuff which will need them.
Over Christmas I was hoping to take a look at exactly what I needed. I was going to treat some theorems as black boxes
Yes, that's why I think Lean is more the future than Isabelle, you can have p-adics and triangulated categories as well as ergodic theory.
Patrick Massot
@PatrickMassot
Ah. One more mathematician to put some pressure on Mario who doesn't like categories ;)
I swear Kevin and I didn't ask Sébastien by another channel
sgouezel
@sgouezel
I don't either, I never use them, but I know some people do.
Mario Carneiro
@digama0
I was looking for a good example, but I'm quite familiar with "explicit proof" - metamath takes explicit to a whole new level (http://us.metamath.org/mpeuni/ostth.html :point_left: Ostrowski's theorem on the absolute values of Q)
I would like to see a way to read tactic proofs actually. It seems like a failure if you can convince the machine but not a human
Patrick Massot
@PatrickMassot
Still, even if you don't use categories, that's in the list of things that came to your mind when thinking about what a proof assistant for the future could handle
Kevin Buzzard
@kbuzzard
Or maybe we need more catchy names for tactics. I like "blast"
I needed a general purpose tactic for my complex number module, and I asked my son for a name and he said "crunch" because apparently this is a Pokemon move
Andrew Ashworth
@alashworth
aren't higher categories the whole point of hott and cubical type theory?
Mario Carneiro
@digama0
already taken
Patrick Massot
@PatrickMassot
blast comes from the Isabelle files we saw today
sgouezel
@sgouezel
This proof of Ostrowski's theorem is definitely explicitly explicit :)
Patrick Massot
@PatrickMassot
Andrew: mathematician have no idea what is Hott and cubical type theory
Kevin Buzzard
@kbuzzard
I guess Voevodsky did
but one might argue
Patrick Massot
@PatrickMassot
Yes, I'm not sure want to be this explicit
It killed him
Kevin Buzzard
@kbuzzard
that he stopped being a mathematician a while ago
Andrew Ashworth
@alashworth
categories are really hard in type theory
as we have now
as i understand it, anyway
Kevin Buzzard
@kbuzzard
This was one reason I suggested schemes be implemented
Andrew Ashworth
@alashworth
and a proof assistant that handled them well would not be lean, it would be some new prover of the future