High School Research

Stream: Lean for teaching

[Eammon Hart]

Another person with a math phd and I teach at a high school that has a math research club. (For context this year the project is something relating to combinatorics and linear algebra that if everything goes well could reasonably be published in an undergrad journal.) We haven’t been very successful in getting freshmen and sophomores involved, so I was thinking of trying to do something with geometry (which all of the freshmen take). More specifically, I was thinking of trying to get them to prove in lean the sum and difference of angles formulas. (The upper class men have all seen this used in the proofs of the derivatives of sine and cosine, so they will also have motivation.)

Lean is pretty far outside of either of our wheel houses (I studied Stochastic processes and my coworker studied Algebraic combinatorics), so I wanted to see if this is a reasonable project idea. I have heard that geometry is unusually hard to code into lean, but I don’t know if that actually means difficult or tedious. If the former its probably not great for high schoolers, but if the later then it could be a good fit. (I am also very open to alternative suggestions.)

Thank you.

[Martin Dvořák]

I have no idea how to do geometry in Lean.

[Kevin Buzzard]

The issue with geometry is that lean is expecting text input in the form of strings, and geometry involves pictures. In particular a proof which appeals to a picture is not going to be easy to do in lean. Perhaps an illustrative example would be the proof known to the ancient Greeks that $\pi>3$: draw a hexagon inside a circle and claim that you're done. Making this into a lean proof would be possible, but rather tricky for a beginner.

Are we talking under 18s here? What do they think of the natural number game? There is plenty of stuff that you can build on from that, for example you can develop a theory of even and odd integers and so on. There are real subtleties here which you only discover when formalising -- for example if you define even to be of the form 2n and odd to be of the form 2n+1 then one needs to prove that every natural is precisely one of even and odd, and this is not immediate, even though it's taken as read at school.

I would like to develop a system accessible to schoolkids where geometry in the style of Euclid can be done in lean but I'm waiting for Joseph Myers' work to be ported to lean 4.

[Eammon Hart]

I haven’t exposed any of them to lean (this was primarily meant as a probe for a potential future project). Yeah they are all under 18. (Youngest this year is 15, but the idea of doing geometry is that we could get the 14 or even 13 years old freshmen into it.) I think that I would have a hard time motivating them parsing the minutia of formalizing the natural numbers. They have to feel like they are in someway contributing to human knowledge and I don’t think that would do the trick for them. I’m pretty sure I could motivate the sum of angles formula, so I was hoping that it would just be a tedious rather than difficult process. (They are already used to tedious column proofs which are somewhat similar in spirit.)

Thanks

[Johan Commelin]

They have to feel like they are in someway contributing to human knowledge

Why? That's a very high bar for HS students if you are looking for maths projects. Unless they only have to feel like they are contributing, without actually contributing.

[Kevin Buzzard]

Teach them how to write tactics in lean 4 if you want them to contribute to human knowledge :-)

[Arthur Paulino]

I'm not a teacher, but as a former HS student, my impression is that the experience with Lean (or any other IPS) would be frustrating and infuriating for most of the students. If you're lucky, you'd get real engagement from 1~3 talented people who are already inclined towards mathematics/computer science.

In my understanding, perceiving numbers through functional lens is a radical paradigm shift that requires a certain degree of mathematical maturity.

As an alternative, have you seen the work from Paul Lockhart? He's been teaching youngsters to reason and prove mathematical properties with a different method. As far as I know, his classes are like discussions, further away from the model in which the teacher delivers knowledge to the students.

[Eammon Hart]

@Johan Commelin I’m aware that they won’t be doing anything groundbreaking, but what they are doing now is genuine research. That allows them to feel like they’re genuinely contributing to human knowledge (even if not that much). @Arthur Paulino is he the mathematicians lament guy? I have not read his stuff. @Kevin Buzzard is the natural numbers game lean 3 or lean 4. I’m not particularly embedded in this stuff, and honestly I’ve been pretty confused trying to figure out how compatible they are and what has been shown to work in which. (And what practical advantages 4 has over 3) I saw a couple of YouTube videos, but as someone who hasn’t taken a logic course in 6 years (and that was undergrad) I didn’t really understand why 4 was so much better than 3.

[Arthur Paulino]

Yes, he is the mathematician lament guy.

Re Lean 3/4: they are not compatible, although the syntax is quite similar. The improvements of Lean 4 over Lean 3 are huge. Lean 4 is a genuine programming language that compiles down to efficient C, also being able to interface with custom C code via the extern flag. Lean 4 also has a more powerful metaprogramming layer.

The Lean 4 compiler is written in Lean 4, opening up amazing possibilities. And there's also Lake, a package manager for Lean 4 that's written in Lean 4.

This is far from being an exhaustive list. But I think I was able to sum up the main advantages I see as a programmer (I don't do much theorem proving)

[Eric Wieser]

@Arthur Paulino has described how Lean 4 is technically superior; but from a practical standpoint, there are many more existing resources available to Lean3 that haven't yet been converted to Lean 4. You might find yourself asking a question about Lean4 for which the answer is "I have some lean3 code that does that that I haven't converted yet".

[Martin Dvořák]

My subjective opinion is that, right now, out-of-the-box Lean 3 is better than out-of-the-box Lean 4.

[Martin Dvořák]

Arthur Paulino said:

(...) perceiving numbers through functional lens is a radical paradigm shift that requires a certain degree of mathematical maturity.

Do you think that this mathematical maturity is acquired by doing mathematical-but-otherwise-unrelated stuff?

[Arthur Paulino]

I think this mathematical maturity is acquired by lots of introspection (at least to me) and contact with different ways to understand functions. When I first studied functions (on my 14's), I thought of them as formulas to transforms numbers into others. Then in discrete mathematics I learned that functions are relations with a specific structure, but I still had the impression that functions served basically to transform a thing into another. Then in Coq/Lean I noticed that function applications can be used to represent things as standalone objects, not necessarily because we want to compute something from another

[Martin Dvořák]

Do you think that mathematicians at some point arrive at a level of mathematical maturity when Lean (or formal proving in general) becomes easy to pick? Even if they never touched a computer during their mathematical studies?

[Arthur Paulino]

It depends on what you mean by "mathematician". Do you mean someone who's at least entered a math undergrad course? I'd say it depends on whether they have visited the basics of type theory or not. For example, the fact that n + m = m + n for any n m : Nat wasn't blindly trivial to the computer was rather frustrating to me at first

[Martin Dvořák]

Yeah. Asking whether math undergrad courses help with understanding Lean later (even with the basics where undergrad knowledge is not explicitly used) is what I was interested in.

[Martin Dvořák]

I think that type theory is not the only background that helps with it. Almost any course on logic will make you encounter Robinson arithmetic or a similar system. Then you clearly see that n + m = m + n is a theorem.

[Arthur Paulino]

But that already raises the entrance bar. Understanding mathematics as a body of knowledge that sits on top of a formal system is a big leap IMO. We're talking about undergrad level of maturity here already.

[Mac Malone]

Arthur Paulino said:

Understanding mathematics as a body of knowledge that sits on top of a formal system is a big leap IMO. We're talking about undergrad level of maturity here already.

I think this also depend on the background curriculum of a given institution. If the school already has had a class on logic or philosophy, students may already be equipped with this paradigm. If not, it is a lot to taken in.

[Mac Malone]

(Oops, sorry for the necropost -- did not realize this topic was months old.)