Skip to main content

CS 22 Lean Reference

Welcome to the CS 22 Lean reference! This website provides an overview of some basic Lean features, style guidelines for writing clear Lean proofs, and an index of the proof tactics used in CS 22. The tactic index will update throughout the semester as new tactics are introduced in lecture. On this page, we provide a summary of what Lean is and why we're using it in 22.

What Is Lean?​

Lean is a kind of program known as an interactive theorem prover. It allows you to construct formal proofs1 about mathematics and checks that those proofs are correct. As the name suggests, it does this interactively: at each step in a proof, Lean shows you what assumptions you currently have to work with (your context) and what remains to be proved (your goals). It automatically checks the correctness of your proof as you construct it and warns you of errors as soon as you make them.

Proofs in Lean are constructed using tactics. These are instructions to Lean that correspond to the kinds of reasoning steps that you take in a paper proof, ranging from modus ponens to simplifying basic arithmetical expressions. Over the course of the semester, we'll introduce you to a small subset of Lean tactics—some of which have been specifically designed for this course—that are relevant to the kinds of math we'll be talking about in this class, like propositional and first-order logic, set theory, and number theory.

While the subset of Lean we'll be working with in 22 has been tailored to this class, it's worth noting that Lean as a system is not just limited to this course or the mathematical topics we cover! The majority of the math that you'll learn as an undergraduate at Brown has been formalized in Lean, along with a wide variety of contemporary mathematical results across virtually every mathematical discipline. (There's even an ongoing effort to formalize Wiles' proof of Fermat's Last Theorem in Lean.)

Lean in CS 22​

Why do we teach Lean in CS 22? Our goal is not for you to become an expert in the Lean language. In fact, many of you will probably never use Lean again after finishing 22.2

Instead, our goal is for Lean to serve as a tool to understand the structure of proofs, the manner in which we construct them, and the types of logical steps we perform in doing so. Lean makes explicit the logical structure of propositions, requires you to specify the precise logical operation you are performing at each step of a proof, and visually renders at every step of a proof what information you have and what claims remain to be shown. While working within such a system may feel constraining, it also reinforces the formal groundwork that underlies the informal arguments that comprise the majority of the proofs you'll see in 22.

Toward this end, we'll try as much as possible not to dive too deeply into the linguistic intricacies of Lean or the technologies or theory on which it's based. Instead, we want to emphasize the "portable" takeaways that translate to, and aid, informal proof-writing: conceptualizing a "proof state" comprising hypotheses and goals; applying introduction and elimination rules corresponding to the connectives and quantifiers at hand; and identifying the proof structure these concepts induce even when rendered in informal prose. (If some—or many—of these words don't make sense right now, don't worry: we'll go over all of this in due time!)

Footnotes​

  1. It's important to note here that formal is not a synonym of rigorous. A formal proof is a proof written in a formalized deductive system according to a set of prescribed logical rules. Precisely defining "deductive system" is beyond the scope of this course, but one intuitive way to think about it is that it's a sort of "very strict language" for writing proofs that is so tightly rule-governed that we can implement a mechanical program (like Lean!) for checking whether a sentence of that language is correct.

    By contrast, proofs that are written not in a deductive system but in natural language (even very precise natural language—what we might call "mathematical English") are called informal proofs. Most proofs you'll encounter in math and CS will be of the informal variety—written as English sentences on textbook pages or lecture slides. Such proofs can still be rigorous, though. When we say a proof is "rigorous," we simply mean that it carefully and correctly articulates its argument. Part of the goal of this course is to teach you to write rigorous informal proofs! ↩

  2. If, however, you end up enjoying Lean and want to learn more about its theory and applications, consider taking CS 1951x in the fall! ↩