Math 7800 Lean Midterm — October 13 corrected release

Take-home Lean midterm: Projects A and B

Released with corrected scaffolds on October 13, 2026. Due Thursday, November 5, 2026, 6pm CST (postponed from October 29), on Gradescope: two .lean files and one PDF write-up. This release replaces the setup-only ZIP.

Start here

  1. Download and unzip the corrected course ZIP into a new local folder. Keep a backup of your existing work; copy your own proofs into the corresponding files without overwriting them accidentally.
  2. Open the folder containing lakefile.toml in VS Code. Use the pinned Lean and Mathlib version, v4.34.0; do not run lake update to upgrade.
  3. Run lake exe cache get if dependencies are not installed yet.
  4. Open Midterm/ProjectA_PiLambda.lean and Midterm/ProjectB_MonotoneClass.lean. Work on them separately: each includes the same frozen definitions and neither imports the other.

From the project root, check each file explicitly:

lake env lean Midterm/ProjectA_PiLambda.lean
lake env lean Midterm/ProjectB_MonotoneClass.lean

A bare lake build checks the introductory library; it does not certify that the midterm is complete. The initial scaffolds deliberately produce five declaration uses sorry warnings each. Replace all five proof placeholders in each file: four scaffold lemmas and the main theorem. There are no scaffold lemmas permitted without proof in a final submission. The #print axioms commands at the end let you check every required declaration. Final proofs must compile without warnings and use only a subset of propext, Classical.choice, and Quot.sound. sorryAx, admit, new axioms, and additional computational trust axioms are not allowed. Compiling with sorry is not a completed verification.

Frozen statements and definitions

Keep the block between BEGIN FROZEN DEFINITIONS and END FROZEN DEFINITIONS unchanged. Keep the namespace Math7800.Midterm, the four lemma names and statements, and the main theorem name and statement unchanged. Add helper lemmas and proofs outside the frozen block as needed. Do not add assumptions or weaken a conclusion. The instructor checker verifies the frozen definitions, statement types, axioms, and Project A’s forbidden dependencies.

IsPiSys requires closure under every pairwise intersection, including an empty intersection of two disjoint members. The generating family itself may be empty. IsLambdaSys contains the whole space, complements, and countable disjoint unions. Monotone classes use natural-number indexed increasing unions and decreasing intersections. These are the conventions for this assignment; numbering a sequence from 0 rather than 1 makes no mathematical difference.

Project A: the four lemmas and the six proof steps

The six steps refer to the proof outline on backup slide 30, not an asserted one-to-one numbering of lemmas in every textbook edition.

Required lemma Meaning Slide 30 steps
lambdaGen_isLambdaSys The generated lambda-system is a lambda-system. 1
subset_lambdaGen The generating family is contained in it. 1
lambdaGen_inter A pi-system generates an intersection-closed lambda-system. 3–4
isSigmaField_of_lambda_pi An intersection-closed lambda-system is a sigma-field. 5

Step 2 supplies helper facts: a lambda-system contains the empty set and is closed under finite disjoint unions (pad a finite list with empty sets). For steps 3–4, use the good-sets argument twice. Step 6 combines the four lemmas with the minimality of the generated systems to prove pi_lambda. You may add and prove helper lemmas for those facts.

You may use general Mathlib set identities and elementary tools such as mem_sInter, sInter_subset_of_mem, disjointed, iUnion_disjointed, disjoint_disjointed, and disjointedRec. You may not use a constant whose name begins with MeasurableSpace.DynkinSystem. or MeasurableSpace.generateFrom, or the constant MeasurableSpace.induction_on_inter. This restriction applies to the compiled proof’s transitive dependencies, including helpers and aliases. It prevents using an existing pi-lambda theorem to prove the assignment.

Project B: the four scaffold lemmas

Required lemma Meaning
monoGen_isMonotoneClass The generated monotone class is a monotone class.
monotone_class_of_sigmaField Every sigma-field is a monotone class.
monoGen_isField A field generates a monotone class that is a field.
isSigmaField_of_field_monotone A field that is a monotone class is a sigma-field.

Use complements and a two-round good-sets argument for finite unions. For countable unions, use increasing finite unions (accumulate) and the monotone class property. Finish monotone_class by proving both inclusions using minimality. General Mathlib tools are allowed; all required declarations still need proofs and a clean axiom audit.

Write-up and help

Explain the proofs in your own words in one PDF, and include an honest self-assessment on the course’s 100-point scale. You may learn with AI; disclosure is not required. What matters is that you can read, write, and explain your Lean code.

Oral check: Thursday, November 12, in class, in four groups of four or five, about 15 minutes per group; the groups are posted before then. Each of you explains one lemma from your own Lean files, chosen by me on the spot, and answers a follow-up question. Everyone scores the other presenters out of 100 on an anonymous peer sheet and fills in a named self-score slip.

The oral grade is individual: one third my score, one third the median peer score, and one third the accuracy of your self score (full credit within 10 points of my score, half credit within 20). If my score is 60 or below, the oral grade is my score alone. If a part is missing (no self-score slip, or no peer scores), the parts that exist share the weight equally. The grading plan is checker 50%, write-up 25%, oral 25%.

Office hours: Tue/Thu 1:00–1:50, STEM+Ag 3147. If a textbook lemma number is unclear, bring its statement and edition so we can match it exactly.