Lean for homework in MOOCs

Stream: new members

[unixguru88]

My name is Jaikrishnan and I am an Assistant professor at Indian Institute of Technology Palakkad. I recently taught a MOOC on real analysis for undergraduates which had several thousand participants. The homework and final exam for this MOOC comprised only objective questions for pragmatic reasons. This is a terrible way to learn real analysis and I was wondering wether it would be feasible to use lean for homework so that students get real practice in proof writing and not just answer objective questions.

[Kevin Buzzard]

The honest answer is that Lean is really great for certain kinds of questions in analysis but quite a chore for others, and if you've never used a theorem prover before then you might be hard-pressed to guess which questions are easy and which are hard. Take a look at the analysis workshop I ran a few weeks ago:

https://github.com/ImperialCollegeLondon/formalising-mathematics/tree/master/src/week_3

I proved things like limit of product is product of limits for a sequence of reals etc.

One thing you have to be aware of though is that it's hard to learn two things at once! My students were people who already knew the mathematics behind all this, so just had to learn the Lean.

If you are interested in discussing using Lean for teaching, there is a stream #Lean for teaching dedicated to this (but feel free to also post in #new members , these are both appropriate places).

[Patrick Massot]

Did you do the tutorial project? It is based on a course for 1st year undergrads.

[unixguru88]

@Patrick Massot Thanks for the pointer! Will have a look.

[unixguru88]

@Kevin Buzzard I do not plan on teaching lean concurrently with real analysis. The idea is to have courses available for the entire undergraduate curriculum for free to everyone. Lean can be the first course that is a prerequisite for all others. I will look through at the analysis workshop to get an idea. Thanks!

[Kevin Sullivan]

unixguru88 said:

Kevin Buzzard I do not plan on teaching lean concurrently with real analysis. The idea is to have courses available for the entire undergraduate curriculum for free to everyone. Lean can be the first course that is a prerequisite for all others. I will look through at the analysis workshop to get an idea. Thanks!

I've also been teaching using Lean. I've found it takes 6-8 weeks for advanced undergraduates and early graduate students to learn the functional programming part: types, values, type universes, inhabited vs uninhabited types (empty), polymorphic container types (box, option, either, list, etc), higher-order recursive function (map, fold, filter etc), and typeclasses, typeclass instances, typeclass inference, and using typeclasses and inference to specify and require the presence of simple algebraic structures, such as monoids and groups. Basically half a semester. And we haven't yet opened the door on logic and proofs. We've been working entirely in (Type u) and not in Prop. My working hypothesis is that the latter will be relatively easy with functional programming foundations in Lean already firm. What I'm saying, is that it takes the better part of a semester to bring students up to speed on Lean and some of its basic applications, whether in formalizing simple abstract mathematics or defining and using new logics, such as Hoare Logic. That's my experience, anyway.

[Patrick Massot]

Very remarkably, in my twelve weeks long course, I mention nothing from your list, not a single item. So clearly we are talking about completely different things. Jaikrishnan, you don't need any of this if you want to use Lean for real analysis proofs, as you can see from the tutorials project. But I'm sure you need them if you want to teach computer science or type theory.

[Kevin Buzzard]

Yes my experience is the same as Patrick -- we never did any maps or filters or even lambda -- we just did tactic mode proofs of undergraduate level mathematics.

[Kevin Sullivan]

Kevin Buzzard said:

Yes my experience is the same as Patrick -- we never did any maps or filters or even lambda -- we just did tactic mode proofs of undergraduate level mathematics.

Interesting. Thanks. I've struggled with a tactic-mode early vs tactic-mode late approach to teaching and have settled on the latter. The hypothesis is that students will better understand what's happening with tactics when we get there. I don't have more than anecdotal data, though.

[Kevin Buzzard]

Are you teaching computer scientists though? I'm teaching mathematicians who in all likelihood have never met a functional language before but can make sense of the natural number game. I can quite believe that teaching computer scientists would require a very different approach.

[Kevin Sullivan]

Kevin Buzzard said:

Are you teaching computer scientists though? I'm teaching mathematicians who in all likelihood have never met a functional language before but can make sense of the natural number game. I can quite believe that teaching computer scientists would require a very different approach.

I am teaching computer scientists. I view Lean (and similarly proof assistants) as providing unified framework for computing with dependent types; and out of that come the abilities it provides to formalize predicate and other logics and higher mathematics within this computational framework. Proof construction is programming. Tactic scripts are programs that build objects of specified types. My sense is that students remain mystified by not knowing what programs tactic scripts specify. That said, it's clearly a matter of application and of empirical hypothesis. There's plenty students can do starting with tactics early. Maybe it's even better. I don't know. I don't think there's any disagreement here, thought the contrast between our approaches is pretty remarkable. For what it's worth, I find there's charm in first fully exposing the computational model (and of course I'm in an environment where it's ok to do this). Once the computational foundation is solid, then we can show them how it can all be applied in ways that are surprising to the CS student: to specify the syntax and semantics of other languages (such as predicate logic), to formalize algebraic structures including the laws that govern them; to formulate and prove theorems in advanced abstract mathematics. I confess that I do have a slightly hard time believing that anyone can excel with a proof assistant without understanding(eventually) it as a programming system. Not only do Lean and others like it make everyday predicate and related logics into special case branches of mathematics; they also make mathematics into a branch of computer science! (Of course everyone from Hilbert on already knew that in a sense.)

[Julian Berman]

It'd sound like a nice corollary if finally programming then is a branch of computer science :D

[Kevin Sullivan]

Julian Berman said:

It'd sound like a nice corollary if finally programming then is a branch of computer science :D

:-) Yes, I'm in the camp that programming, understood as the study of how one can best wield mathematical/logical expression to effectively represent things of interest in some domain, is a branch of computer science. Mere practical program development these days is applied computer science but pretty well understood. What we still don't understand how to do well enough in practice is to "get it sufficiently right." See, for example, the latest devastating security breaches across government and industry in the US. The programming we've been doing for 70 years at this point isn't really working to provide solid foundations for major national and world infrastructure systems. Maybe the fact that we've left Prop out of every popular programming language is part of the problem. (There are other problems, too; notably software today comes without explicit interpretations, in the sense of interpretations/denotations in the semantics of, say, predicate logic. The code thus remains stripped of domain content and constraints, and so can perform all kinds of actions that make no sense semantically, in the actual application domain. But this is a topic for another day, also linked to Lean and the like, but out of bounds for the original post.)

[Scott Morrison]

I wonder if in the "teaching tactics late" approach show_term { ... } is a useful thing to introduce to students. I think it help a lot to see that every tactic step is just producing a term, possibly with holes.

[Kevin Buzzard]

Next year I was considering teaching basic logic proofs with tactic intro, apply, split, exact stuff, and then when they've got the hang of it just having a one-off lesson on what a lambda-term looks like and how they've been making them all along.

[Kevin Sullivan]

Scott Morrison said:

I wonder if in the "teaching tactics late" approach show_term { ... } is a useful thing to introduce to students. I think it help a lot to see that every tactic step is just producing a term, possibly with holes.

I do make working with holes an integral element of my computation-first approach. We call it, type-guided, top-down refinement, also known in the old days as "structured programming." We're also constantly looking at contexts and goals, as a way to "be guided by the types."

[Kevin Buzzard]

Yes, you are thinking about things on a far more foundational level. For me the fundamental question is not "how does Lean's type theory work?" but "how do I turn this standard mathematical result that a product of limits is a limit of the products into Lean tactic code?" The student still sees the basic principle that there are holes which need to be filled, but in the context of a changing tactic goal which can be interpreted as a (sometimes high-powered) mathematical statement rather than as a term in a type theory.

[Kevin Sullivan]

Kevin Buzzard said:

Yes, you are thinking about things on a far more foundational level. For me the fundamental question is not "how does Lean's type theory work?" but "how do I turn this standard mathematical result that a product of limits is a limit of the products into Lean tactic code?" The student still sees the basic principle that there are holes which need to be filled, but in the context of a changing tactic goal which can be interpreted as a (sometimes high-powered) mathematical statement rather than as a term in a type theory.

For what it's worth, I don't think of myself as answering the question, "How does Lean's type theory work?" Rather it's (1) How do you program effectively in Lean? What affordances does it provide to the programmer? That's where the list above comes from: inductive types, the definition of functions by cases, parametric polymorphism, ad hoc polymorphism/typeclasses, dependent types (Pi and Sigma types as examples), and then, of course, programming in Prop, where the only thing that matters is being inhabited; (2) how can these constructs be used to define language syntax and semantics, to define syntax and semantics of various logics, to embed and check rules/invariants expressed in such languages in data types , and to use these capabilities to formalize and "computerize" mathematics? (3) How to prove that given solutions comply with given rules. (4) the idea that proofs in Lean are programs (not just "terms in type theory), and so their production is an exercise in programming; (5) type-guided top-down and bottom up structured program refinement/composition; (6) the concept of program synthesis, which is to say the use of various clever procedures to automatically complete parts of programs, and thus tactics/meta-programming.

You're right of course that this material is more foundational that what you're teaching, which starts with (1) a rich library of pre-defined types and values with which to program, particularly designed for formalization of mathematics; (2) tactic languages as higher-level, albeit somwhat kludgy, programming languages.

This is a useful conversation for me, because it sharpens my understanding of what a tactics-first approach brings to students early that my more basic programming approach doesn't, and that's partial program synthesis capabilities via meta-programs abstracted as tactics. I can see why one would want to deliver that capability to students early, so that they can actually get stuff done that's meaningful in their domain, e.g., of algebra, without having to lean the basics. Pedagogically that can be inspiring, to see what can be done even by a beginner.

One problem with this approach that I can see is that meta-program-based, type-driven program-synthesis libraries, i.e, tactic languages, (beyond the level of tactics that are just syntactic sugars for basic programming mechanisms such as lambda abstraction and function application with unspecified arguments (holes)) are somewhat ad hoc and irregular: not especially well designed as programming languages, per se. So it can seem that one is trying to master a collection of sometimes complex and arbitrary programming abstractions rather than simple basic building blocks; but that's generally the nature of programming against a library, in general.

[Mario Carneiro]

(4) the idea that proofs in Lean are programs (not just "terms in type theory), and so their production is an exercise in programming;

I actually think that lean repudiates this principle more than it validates it. If you were working in no-axioms Coq or cubical type theory or something like that then you can make this claim that all proofs are computable, but in lean the majority of definitions are either proofs or programs but very rarely both. All our programs, that are intended to be executed efficiently, have very simple types for the most part, such that their "proof content" is essentially trivial; and the majority of proofs in mathlib are (1) inhabiting members of Prop, which is a computationally irrelevant type, so executing them is meaningless, and (2) mostly make use of noncomputable axioms like the axiom of choice, which can't be executed anyway.

[Scott Morrison]

not especially well designed as programming languages

This is very fair criticism of what you see going on inside begin ... end blocks. I wouldn't know how to start improving it, however.

[Mario Carneiro]

I would argue that lean 4 has taken some concrete steps toward improving the structure of tactic proofs