diff --git a/100.html b/100.html index 27c8721904..3164f70f86 100644 --- a/100.html +++ b/100.html @@ -62,7 +62,7 @@
1. The Irrationality of the Square Root
theorem irrational_sqrt_two :
Irrational (Real.sqrt 2)
-

docs, source

+

docs, source

@@ -77,7 +77,7 @@
2. Fundamental Theorem of Algebra (hf : 0 < Polynomial.degree f) :
∃ z, Polynomial.IsRoot f z
-

docs, source

+

docs, source

@@ -88,7 +88,7 @@
3. The Denumerability of the Rational N
instance Rat.instDenumerableRat :
Denumerable ℚ
-

docs, source

+

docs, source

@@ -117,7 +117,7 @@
4. Pythagorean Theorem (p3 : P) :
dist p1 p3 * dist p1 p3 = dist p1 p2 * dist p1 p2 + dist p3 p2 * dist p3 p2 ↔ EuclideanGeometry.angle p1 p2 p3 = Real.pi / 2
-

docs, source

+

docs, source

@@ -142,7 +142,7 @@
7. Law of Quadratic Reciprocity (hpq : p ≠ q) :
legendreSym q ↑p * legendreSym p ↑q = (-1) ^ (p / 2 * (q / 2))
-

docs, source

+

docs, source

theorem jacobiSym.quadratic_reciprocity @@ -154,7 +154,7 @@
7. Law of Quadratic Reciprocity (hb : Odd b) :
jacobiSym (↑a) b = (-1) ^ (a / 2 * (b / 2)) * jacobiSym (↑b) a
-

docs, source

+

docs, source

@@ -178,7 +178,7 @@
10. Euler’s Generalization of Fermat (h : Nat.Coprime x n) :
x ^ Nat.totient n ≡ 1 [MOD n]
-

docs, source

+

docs, source

@@ -191,7 +191,7 @@
11. The Infinitude of Primes Nat.exists_infinite_primes (n : ℕ) :
∃ p, n ≤ p ∧ Nat.Prime p
-

docs, source

+

docs, source

@@ -202,7 +202,7 @@
14. Euler’s Summation of 1 + (1/2)^2
theorem hasSum_zeta_two :
HasSum (fun n => 1 / ↑n ^ 2) (Real.pi ^ 2 / 6)
-

docs, source

+

docs, source

@@ -235,7 +235,7 @@
15. Fundamental Theorem of Integral Ca (hb : Filter.Tendsto f (nhds b ⊓ MeasureTheory.Measure.ae MeasureTheory.volume) (nhds c)) :
HasStrictDerivAt (fun u => ∫ (x : ℝ) in a..u, f x) c b
-

docs, source

+

docs, source

theorem intervalIntegral.integral_eq_sub_of_hasDeriv_right_of_le @@ -263,7 +263,7 @@
15. Fundamental Theorem of Integral Ca (f'int : IntervalIntegrable f' MeasureTheory.volume a b) :
∫ (y : ℝ) in a..b, f' y = f b - f a
-

docs, source

+

docs, source

@@ -285,7 +285,7 @@
17. De Moivre’s Formula (z : ℂ) :
(Complex.cos z + Complex.sin z * Complex.I) ^ n = Complex.cos (↑n * z) + Complex.sin (↑n * z) * Complex.I
-

docs, source

+

docs, source

@@ -300,7 +300,7 @@
18. Liouville’s Theorem and the Cons (lx : Liouville x) :
Transcendental ℤ x
-

docs, source

+

docs, source

@@ -313,7 +313,7 @@
19. Four Squares Theorem Nat.sum_four_squares (n : ℕ) :
∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = n
-

docs, source

+

docs, source

@@ -330,7 +330,7 @@
20. All Primes (1 mod 4) Equal the Sum (hp : p % 4 ≠ 3) :
∃ a b, a ^ 2 + b ^ 2 = p
-

docs, source

+

docs, source

@@ -341,7 +341,7 @@
22. The Non-Denumerability of the Cont
theorem Cardinal.not_countable_real :
¬Set.Countable Set.univ
-

docs, source

+

docs, source

@@ -359,7 +359,7 @@
23. Formula for Pythagorean Triples {z : ℤ} :
PythagoreanTriple x y z ↔ ∃ k m n, (x = k * (m ^ 2 - n ^ 2) ∧ y = k * (2 * m * n) ∨ x = k * (2 * m * n) ∧ y = k * (m ^ 2 - n ^ 2)) ∧ (z = k * (m ^ 2 + n ^ 2) ∨ z = -k * (m ^ 2 + n ^ 2))
-

docs, source

+

docs, source

@@ -389,7 +389,7 @@
25. Schroeder-Bernstein Theorem (hg : Function.Injective g) :
∃ h, Function.Bijective h
-

docs, source

+

docs, source

@@ -400,7 +400,7 @@
26. Leibniz’s Series for Pi
theorem Real.tendsto_sum_pi_div_four :
Filter.Tendsto (fun k => Finset.sum (Finset.range k) fun i => (-1) ^ i / (2 * ↑i + 1)) Filter.atTop (nhds (Real.pi / 4))
-

docs, source

+

docs, source

@@ -433,7 +433,7 @@
27. Sum of the Angles of a Triangle (h3 : p3 ≠ p1) :
EuclideanGeometry.angle p1 p2 p3 + EuclideanGeometry.angle p2 p3 p1 + EuclideanGeometry.angle p3 p1 p2 = Real.pi
-

docs, source

+

docs, source

@@ -458,7 +458,7 @@
34. Divergence of the Harmonic Series
theorem Real.tendsto_sum_range_one_div_nat_succ_atTop :
Filter.Tendsto (fun n => Finset.sum (Finset.range n) fun i => 1 / (↑i + 1)) Filter.atTop Filter.atTop
-

docs, source

+

docs, source

@@ -484,7 +484,7 @@
35. Taylor’s Theorem (hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Set.Icc x₀ x)) (Set.Ioo x₀ x)) :
∃ x' x_1, f x - taylorWithinEval f n (Set.Icc x₀ x) x₀ x = iteratedDerivWithin (n + 1) f (Set.Icc x₀ x) x' * (x - x₀) ^ (n + 1) / ↑(Nat.factorial (n + 1))
-

docs, source

+

docs, source

theorem taylor_mean_remainder_cauchy @@ -503,7 +503,7 @@
35. Taylor’s Theorem (hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Set.Icc x₀ x)) (Set.Ioo x₀ x)) :
∃ x' x_1, f x - taylorWithinEval f n (Set.Icc x₀ x) x₀ x = iteratedDerivWithin (n + 1) f (Set.Icc x₀ x) x' * (x - x') ^ n / ↑(Nat.factorial n) * (x - x₀)
-

docs, source

+

docs, source

@@ -542,7 +542,7 @@
38. Arithmetic Mean/Geometric Mean (hz : ∀ (i : ι), i ∈ s → 0 ≤ z i) :
(Finset.prod s fun i => z i ^ w i) ≤ Finset.sum s fun i => w i * z i
-

docs, source

+

docs, source

@@ -563,7 +563,7 @@
39. Solutions to Pell’s Equation (hp : x * x - Pell.d a1 * y * y = 1) :
∃ n, x = Pell.xn a1 n ∧ y = Pell.yn a1 n
-

docs, source

+

docs, source

theorem Pell.exists_of_not_isSquare @@ -573,7 +573,7 @@
39. Solutions to Pell’s Equation (hd : ¬IsSquare d) :
∃ x y, x ^ 2 - d * y ^ 2 = 1 ∧ y ≠ 0
-

docs, source

+

docs, source

In pell.eq_pell, d is defined to be a*a - 1 for an arbitrary a > 1.

@@ -616,7 +616,7 @@
40. Minkowski’s Fundamental Theorem (h_conv : Convex ℝ s) :
∃ x x_1, ↑x ∈ s
-

docs, source

+

docs, source

@@ -644,7 +644,7 @@
44. The Binomial Theorem (n : ℕ) :
(x + y) ^ n = Finset.sum (Finset.range (n + 1)) fun m => x ^ m * y ^ (n - m) * ↑(Nat.choose n m)
-

docs, source

+

docs, source

@@ -674,7 +674,7 @@
49. The Cayley-Hamilton Theorem (M : Matrix n n R) :
↑(Polynomial.aeval M) (Matrix.charpoly M) = 0
-

docs, source

+

docs, source

@@ -689,7 +689,7 @@
51. Wilson’s Lemma [Fact (Nat.Prime p)] :
↑(Nat.factorial (p - 1)) = -1
-

docs, source

+

docs, source

@@ -704,7 +704,7 @@
52. The Number of Subsets of a Set (s : Finset α) :
Finset.card (Finset.powerset s) = 2 ^ Finset.card s
-

docs, source

+

docs, source

@@ -750,7 +750,7 @@
55. Product of Segments of Chords (hcpd : EuclideanGeometry.angle c p d = Real.pi) :
dist a p * dist b p = dist c p * dist d p
-

docs, source

+

docs, source

@@ -774,7 +774,7 @@
58. Formula for the Number of Combinat (s : Finset α) :
Finset.card (Finset.powersetCard n s) = Nat.choose (Finset.card s) n
-

docs, source

+

docs, source

theorem Finset.mem_powersetCard @@ -786,7 +786,7 @@
58. Formula for the Number of Combinat {t : Finset α} :
s ∈ Finset.powersetCard n t ↔ s ⊆ t ∧ Finset.card s = n
-

docs, source

+

docs, source

@@ -824,7 +824,7 @@
59. The Laws of Large Numbers (hident : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (X i) (X 0)) :
∀ᵐ (ω : Ω), Filter.Tendsto (fun n => (↑n)⁻¹ • Finset.sum (Finset.range n) fun i => X i ω) Filter.atTop (nhds (∫ (a : Ω), X 0 a))
-

docs, source

+

docs, source

@@ -839,7 +839,7 @@
60. Bezout’s Theorem (y : ℕ) :
↑(Nat.gcd x y) = ↑x * Nat.gcdA x y + ↑y * Nat.gcdB x y
-

docs, source

+

docs, source

@@ -871,7 +871,7 @@
62. Fair Games Theorem τ ≤ π → (∃ N, ∀ (x : Ω), π x ≤ N) → ∫ (x : Ω), MeasureTheory.stoppedValue f τ x ∂μ ≤ ∫ (x : Ω), MeasureTheory.stoppedValue f π x ∂μ -

docs, source

+

docs, source

@@ -884,7 +884,7 @@
63. Cantor’s Theorem Cardinal.cantor (a : Cardinal.{u}) :
a < 2 ^ a
-

docs, source

+

docs, source

@@ -913,7 +913,7 @@
64. L’Hopital’s Rule (hdiv : Filter.Tendsto (fun x => deriv f x / deriv g x) (nhds a) l) :
Filter.Tendsto (fun x => f x / g x) (nhdsWithin a {a}ᶜ) l
-

docs, source

+

docs, source

@@ -944,7 +944,7 @@
65. Isosceles Triangle Theorem (h : dist p1 p2 = dist p1 p3) :
EuclideanGeometry.angle p1 p2 p3 = EuclideanGeometry.angle p1 p3 p2
-

docs, source

+

docs, source

@@ -969,7 +969,7 @@
66. Sum of a Geometric Series (hmn : m ≤ n) :
(Finset.sum (Finset.Ico m n) fun i => x ^ i) = (x ^ n - x ^ m) / (x - 1)
-

docs, source

+

docs, source

theorem NNReal.hasSum_geometric @@ -977,7 +977,7 @@
66. Sum of a Geometric Series (hr : r < 1) :
HasSum (fun n => r ^ n) (1 - r)⁻¹
-

docs, source

+

docs, source

@@ -997,7 +997,7 @@
68. Sum of an arithmetic series Finset.sum_range_id (n : ℕ) :
(Finset.sum (Finset.range n) fun i => i) = n * (n - 1) / 2
-

docs, source

+

docs, source

@@ -1018,7 +1018,7 @@
69. Greatest Common Divisor Algorithm (b : R) :
R
-

docs, source

+

docs, source

theorem EuclideanDomain.gcd_dvd @@ -1032,7 +1032,7 @@
69. Greatest Common Divisor Algorithm (b : R) :
EuclideanDomain.gcd a b ∣ a ∧ EuclideanDomain.gcd a b ∣ b
-

docs, source

+

docs, source

theorem EuclideanDomain.dvd_gcd @@ -1048,7 +1048,7 @@
69. Greatest Common Divisor Algorithm {c : R} :
c ∣ a → c ∣ b → c ∣ EuclideanDomain.gcd a b
-

docs, source

+

docs, source

@@ -1076,7 +1076,7 @@
71. Order of a Subgroup [Fintype { x // x ∈ s }] :
Fintype.card { x // x ∈ s } ∣ Fintype.card α
-

docs, source

+

docs, source

@@ -1101,7 +1101,7 @@
72. Sylow’s Theorem (hdvd : p ^ n ∣ Fintype.card G) :
∃ K, Fintype.card { x // x ∈ K } = p ^ n
-

docs, source

+

docs, source

sylow_conjugate

card_sylow_dvd

card_sylow_modeq_one

@@ -1142,7 +1142,7 @@
75. The Mean Value Theorem (hfd : DifferentiableOn ℝ f (Set.Ioo a b)) :
∃ c, c ∈ Set.Ioo a b ∧ deriv f c = (f b - f a) / (b - a)
-

docs, source

+

docs, source

@@ -1167,7 +1167,7 @@
76. Fourier Series (n : ℤ) :
E
-

docs, source

+

docs, source

theorem hasSum_fourier_series_L2 @@ -1177,7 +1177,7 @@
76. Fourier Series (f : { x // x ∈ MeasureTheory.Lp ℂ 2 }) :
HasSum (fun i => fourierCoeff (↑↑f) i • fourierLp 2 i) f
-

docs, source

+

docs, source

@@ -1192,7 +1192,7 @@
77. Sum of kth powers (p : ℕ) :
(Finset.sum (Finset.range n) fun k => ↑k ^ p) = Finset.sum (Finset.range (p + 1)) fun i => bernoulli i * ↑(Nat.choose (p + 1) i) * ↑n ^ (p + 1 - i) / (↑p + 1)
-

docs, source

+

docs, source

theorem sum_Ico_pow @@ -1200,7 +1200,7 @@
77. Sum of kth powers (p : ℕ) :
(Finset.sum (Finset.Ico 1 (n + 1)) fun k => ↑k ^ p) = Finset.sum (Finset.range (p + 1)) fun i => bernoulli' i * ↑(Nat.choose (p + 1) i) * ↑n ^ (p + 1 - i) / (↑p + 1)
-

docs, source

+

docs, source

@@ -1225,7 +1225,7 @@
78. The Cauchy-Schwarz Inequality (y : E) :
‖inner x y‖ * ‖inner y x‖ ≤ ↑IsROrC.re (inner x x) * ↑IsROrC.re (inner y y)
-

docs, source

+

docs, source

theorem norm_inner_le_norm @@ -1243,7 +1243,7 @@
78. The Cauchy-Schwarz Inequality (y : E) :
‖inner x y‖ ≤ ‖x‖ * ‖y‖
-

docs, source

+

docs, source

@@ -1282,7 +1282,7 @@
79. The Intermediate Value Theorem (hf : ContinuousOn f (Set.Icc a b)) :
Set.Icc (f a) (f b) ⊆ f '' Set.Icc a b
-

docs, source

+

docs, source

@@ -1301,11 +1301,11 @@
80. The Fundamental Theorem of Arithme (h₂ : ∀ (p : ℕ), p ∈ l → Nat.Prime p) :
l ~ Nat.factors n
-

docs, source

+

docs, source

instance Int.euclideanDomain :
EuclideanDomain ℤ
-

docs, source

+

docs, source

instance EuclideanDomain.to_principal_ideal_domain @@ -1313,7 +1313,7 @@
80. The Fundamental Theorem of Arithme [EuclideanDomain R] :
IsPrincipalIdealRing R
-

docs, source

+

docs, source

class UniqueFactorizationMonoid @@ -1323,7 +1323,7 @@
80. The Fundamental Theorem of Arithme extends WfDvdMonoid :
Prop
-

docs, source

+

docs, source

theorem UniqueFactorizationMonoid.factors_unique @@ -1343,7 +1343,7 @@
80. The Fundamental Theorem of Arithme (h : Associated (Multiset.prod f) (Multiset.prod g)) :
Multiset.Rel Associated f g
-

docs, source

+

docs, source

it also has a generalized version, by showing that every Euclidean domain is a unique factorization domain, and showing that the integers form a Euclidean domain.

@@ -1377,7 +1377,7 @@
85. Divisibility by 3 Rule Nat.three_dvd_iff (n : ℕ) :
3 ∣ n ↔ 3 ∣ List.sum (Nat.digits 10 n)
-

docs, source

+

docs, source

@@ -1390,7 +1390,7 @@
86. Lebesgue Measure and Integration < MeasureTheory.lintegral {α : Type u_5} :
{x : MeasurableSpace α} → MeasureTheory.Measure α → (α → ENNReal) → ENNReal
-

docs, source

+

docs, source

@@ -1407,13 +1407,13 @@
88. Derangements Formula [DecidableEq α] :
Fintype.card ↑(derangements α) = numDerangements (Fintype.card α)
-

docs, source

+

docs, source

theorem numDerangements_sum (n : ℕ) :
↑(numDerangements n) = Finset.sum (Finset.range (n + 1)) fun k => (-1) ^ k * ↑(Nat.ascFactorial k (n - k))
-

docs, source

+

docs, source

@@ -1432,7 +1432,7 @@
89. The Factor and Remainder Theorems {p : Polynomial R} :
Polynomial.X - ↑Polynomial.C a ∣ p ↔ Polynomial.IsRoot p a
-

docs, source

+

docs, source

theorem Polynomial.mod_X_sub_C_eq_C_eval @@ -1444,7 +1444,7 @@
89. The Factor and Remainder Theorems (a : R) :
p % (Polynomial.X - ↑Polynomial.C a) = ↑Polynomial.C (Polynomial.eval a p)
-

docs, source

+

docs, source

@@ -1455,7 +1455,7 @@
90. Stirling’s Formula
theorem Stirling.tendsto_stirlingSeq_sqrt_pi :
Filter.Tendsto (fun n => Stirling.stirlingSeq n) Filter.atTop (nhds (Real.sqrt Real.pi))
-

docs, source

+

docs, source

@@ -1474,7 +1474,7 @@
91. The Triangle Inequality (b : E) :
‖a + b‖ ≤ ‖a‖ + ‖b‖
-

docs, source

+

docs, source

@@ -1510,7 +1510,7 @@
94. The Law of Cosines (p3 : P) :
dist p1 p3 * dist p1 p3 = dist p1 p2 * dist p1 p2 + dist p3 p2 * dist p3 p2 - 2 * dist p1 p2 * dist p3 p2 * Real.cos (EuclideanGeometry.angle p1 p2 p3)
-

docs, source

+

docs, source

@@ -1549,7 +1549,7 @@
95. Ptolemy’s Theorem (hbpd : EuclideanGeometry.angle b p d = Real.pi) :
dist a b * dist c d + dist b c * dist d a = dist a c * dist b d
-

docs, source

+

docs, source

@@ -1581,7 +1581,7 @@
97. Cramer’s Rule (b : n → α) :
Matrix.mulVec A (↑(Matrix.cramer A) b) = Matrix.det A • b
-

docs, source

+

docs, source

@@ -1596,7 +1596,7 @@
98. Bertrand’s Postulate (hn0 : n ≠ 0) :
∃ p, Nat.Prime p ∧ n < p ∧ p ≤ 2 * n
-

docs, source

+

docs, source

diff --git a/mathlib_stats.html b/mathlib_stats.html index 7fdfb87101..40c3dcfc89 100644 --- a/mathlib_stats.html +++ b/mathlib_stats.html @@ -81,7 +81,7 @@

Counts

70411 - 126331 + 126333 310 diff --git a/teaching/courses.html b/teaching/courses.html index 17ed282e2a..e8676947bd 100644 --- a/teaching/courses.html +++ b/teaching/courses.html @@ -93,8 +93,12 @@

Courses using Lean

computer science +functional programming + intro to proof +intro to proofs + logic mathematics @@ -153,62 +157,66 @@

Courses using Lean

- Jakob von RaumerTheorem Prover Lab -- Applications in Programming LanguagesKarlsruhe Institute of Technology2022German, advanced, computer science, lean4 + Martin DvorakProgramování a dokazování v Leanuonline2022functional programming, intro to proofs, lean4 - Matthew BallardTransition to Advanced MathematicsUniversity of South Carolina2022intro to proof, mathematics, lean4 + Jakob von RaumerTheorem Prover Lab -- Applications in Programming LanguagesKarlsruhe Institute of Technology2022German, advanced, computer science, lean4 - Jeremy AvigadLogic and Mechanized ReasoningCarnegie Mellon University2021advanced, automated reasoning, logic, lean4 + Matthew BallardTransition to Advanced MathematicsUniversity of South Carolina2022intro to proof, mathematics, lean4 - Frédéric Tran MinhComplement to general Analysis/Algebra 1st year undergraduate courseEsisar, Grenoble Institute of Technology2023French, intro to proof, mathematics, lean3 + Jeremy AvigadLogic and Mechanized ReasoningCarnegie Mellon University2021advanced, automated reasoning, logic, lean4 - Kevin BuzzardFormalising Mathematics 2023Imperial College London2023advanced, mathematics, lean3 + Frédéric Tran MinhComplement to general Analysis/Algebra 1st year undergraduate courseEsisar, Grenoble Institute of Technology2023French, intro to proof, mathematics, lean3 - Patrick KinnearLean learning group 2023Glasgow-Maxwell School2023advanced, mathematics, lean3 + Kevin BuzzardFormalising Mathematics 2023Imperial College London2023advanced, mathematics, lean3 - Robert Y. Lewis, Jasmin Blanchette, Anne BaanenLogic and ModellingVrije Universiteit Amsterdam2023computer science, intro to proof, logic, lean3 + Bjørn Kjos-HanssenGraduate Introduction to LogicUniversity of Hawaii at Manoa2023advanced, logic, mathematics, lean3 - Patrick MassotLogique et démonstrations assistées par ordinateurUniversité Paris-Saclay2023French, intro to proof, natural language input, lean3 + Patrick KinnearLean learning group 2023Glasgow-Maxwell School2023advanced, mathematics, lean3 - Peter PfaffelhuberSome high-school mathematics in LeanUniversity of Freiburg, Germany2023German, intro to proof, mathematics, lean3 + Robert Y. Lewis, Jasmin Blanchette, Anne BaanenLogic and ModellingVrije Universiteit Amsterdam2023computer science, intro to proof, logic, lean3 - Miguel MarcoTopoloía generalUniversidad de Zaragoza2023Spanish, mathematics, lean3 + Patrick MassotLogique et démonstrations assistées par ordinateurUniversité Paris-Saclay2023French, intro to proof, natural language input, lean3 - Bjørn Kjos-HanssenGraduate Introduction to LogicUniversity of Hawaii at Manoa2022advanced, logic, mathematics, lean3 + Peter PfaffelhuberSome high-school mathematics in LeanUniversity of Freiburg, Germany2023German, intro to proof, mathematics, lean3 - Jeremy AvigadInteractive Theorem ProvingCarnegie Mellon University2022mathematics, lean3 + Miguel MarcoTopoloía generalUniversidad de Zaragoza2023Spanish, mathematics, lean3 - Sina HazratpourIntroduction to Proofs with Lean Proof AssistantJohns Hopkins University2022intro to proof, mathematics, lean3 + Jeremy AvigadInteractive Theorem ProvingCarnegie Mellon University2022mathematics, lean3 - Gihan MarasinghaModern Mathematics with LeanUniversity of Exeter2022intro to proof, logic, mathematics, lean3 + Sina HazratpourIntroduction to Proofs with Lean Proof AssistantJohns Hopkins University2022intro to proof, mathematics, lean3 + Gihan MarasinghaModern Mathematics with LeanUniversity of Exeter2022intro to proof, logic, mathematics, lean3 + + + Jeremy AvigadLogic and ProofCarnegie Mellon University2017intro to proof, logic, lean3 @@ -362,18 +370,22 @@
Contributing
`, website: "http://math.iisc.ac.in/~gadgil/proofs-and-programs-2023/", material: "http://math.iisc.ac.in/~gadgil/proofs-and-programs-2023/doc/PnP2023.html", repository: "https://github.com/siddhartha-gadgil/proofs-and-programs-2023", notes: `None`, experiences: `

My plan was to live code, then clean-up and add documentation and generate notes with DocGen4. This worked very well for a month, with a lot of questions and my adapting explanations. Once the projects started the decoupling of lectures and evaluation led to a sharp drop in attendance. I course corrected and made lectures into project demo/help/live-coding. Advanced students explaining what they had done and less advanced explained what they had, where they were stuck, what they needed etc and I (and their fellow students) helped them get unstuck. This is working well. Next time I teach I will transition earlier and in a more planned way to this mode.

` }, - 10: { summary: `

Masters course for computer science students with the first half of the term consisting of a hands-on introduction to Lean 4 and type theory and the second half consisting of the students working on either a semantics/compiler project or a formalisation of a graph theory problem.

+ 10: { summary: `

We are a korespondenční seminář (lit. "correspondence seminar" in the sense of a seminar arranged by exchanging letters and emails) called M&M, which is something like an online course for math-olympiad highschoolers, under the hood of the Faculty of Mathematics and Physics of Charles University in Prague. All our texts are written in Czech; it is also the language of our in-person meetings. Lean is one of our three topics for the school year 2023/2024. There will be five volumes with Lean assignments, six volumes in total. We use Lean 4. Syllabus: (1) the very basics of functional programming; (2) lists; (3) elementary algebraic manipulations; (4) logic; (5) induction.

+`, website: "https://mam.mff.cuni.cz/", material: "None", repository: "https://github.com/madvorak/lean-mam", notes: `None`, experiences: `

We currently have 41 active participants (counting students who solved at least three Lean exercises). Grading solutions doesn't take much time. Creating materials does.

+` }, + + 11: { summary: `

Masters course for computer science students with the first half of the term consisting of a hands-on introduction to Lean 4 and type theory and the second half consisting of the students working on either a semantics/compiler project or a formalisation of a graph theory problem.

`, website: "https://pp.ipd.kit.edu/lehre/SS2022/tba/?lang=de", material: "None", repository: "https://github.com/IPDSnelting/tba-2022", notes: `

The website is partially German, includes more slides and the project descriptions.

`, experiences: `

This was already the second year we used Lean 4 and it was good to do it in person again after teaching exclusively online due to Covid the year before. We had different levels of learning speed among the students but in the end everybody go the point where they intuitively could use Lean. Some students were really eager to golf every proof.

` }, - 11: { summary: `

Our intro to proofs course. (Fall 2020) Lean was about 1/3 of the course. (Fall 2022) A second iteration using Lean 4.

+ 12: { summary: `

Our intro to proofs course. (Fall 2020) Lean was about 1/3 of the course. (Fall 2022) A second iteration using Lean 4.

`, website: "https://300.f22.matthewrobertballard.com/", material: "None", repository: "None", notes: `None`, experiences: `None` }, - 12: { summary: `

This course introduces students to the theory of propositional and first-order logic, shows them how to implement fundamental logical algorithms in Lean 4, and shows them how to use automated reasoning tools.

+ 13: { summary: `

This course introduces students to the theory of propositional and first-order logic, shows them how to implement fundamental logical algorithms in Lean 4, and shows them how to use automated reasoning tools.

`, website: "https://www.cs.cmu.edu/~mheule/15217-f21/", material: "https://avigad.github.io/lamr/logic_and_mechanized_reasoning.pdf", repository: "https://github.com/avigad/lamr", notes: `None`, experiences: `None` }, - 13: { summary: `

Short module introducing proof to 1st year undergraduates using Lean3 - in French. We used proof-term style in Lean.

+ 14: { summary: `

Short module introducing proof to 1st year undergraduates using Lean3 - in French. We used proof-term style in Lean.

`, website: "None", material: "None", repository: "https://github.com/ftranminh/Esisar_MA121_HA_lean_2023", notes: `

1st year students, 6 x 1,5h

`, experiences: ` ` }, - 14: { summary: `

The course is project-based; the students must write three projects on undergraduate mathematics. The lectures are me live Lean coding, solving the sorrys in the repo. I'm teaching the course again in 2024 and then it will be in Lean 4.

+ 15: { summary: `

The course is project-based; the students must write three projects on undergraduate mathematics. The lectures are me live Lean coding, solving the sorrys in the repo. I'm teaching the course again in 2024 and then it will be in Lean 4.

`, website: "https://www.ma.imperial.ac.uk/~buzzard/xena/formalising-mathematics-2023/index.html", material: "None", repository: "https://github.com/ImperialCollegeLondon/formalising-mathematics-2023", notes: `None`, experiences: `None` }, - 15: { summary: `

A 1-semester course aimed at graduate students in algebra and related topics at Edinburgh, Heriot-Watt and Glasgow universities. Aimed to approach Lean as mathematicians and future formalisers, establishing proficiency in tactic mode. For the first part of the course we learned the basics of first-order logic in Lean using the tutorials project, before discussing some basics of types and type classes to talk about formalising algebra. Also made use of lftcm2020 exercise sheets, and MiL. Concluded with a hackathon working on some group projects.

+ 16: { summary: `

A graduate course in mathematical logic taken mostly by MA and PhD students in mathematics and offered every other year (Fall 2016+2n, n=0,1,2,3,4). Model theory, computability theory, set theory. In particular syntax and semantics of first order logic; incompleteness, completeness, and compactness theorems; Loewenheim-Skolem theorems; computable and computably enumerable sets; axioms of set theory; ordinals and cardinals. Since 2020 I include Lean exercises and projects, and some discussion of type theory. For example, formalization of part of Gödel's theorems is included at https://github.com/bjoernkjoshanssen/math654/blob/main/g%C3%B6del-beta-homework.lean

+`, website: "https://math.hawaii.edu/wordpress/bjoern/math-654-fall-2022/", material: "None", repository: "https://github.com/bjoernkjoshanssen/math654", notes: `None`, experiences: `

The students are willing and able to learn Lean. Including Lean showcases logic as a vibrant rather than dormant area of study. As projects in 2022 students created formalizations of exercise solutions for my book "Automatic complexity", some of which are included at https://github.com/bjoernkjoshanssen/diophantine-lemma

+` }, + + 17: { summary: `

A 1-semester course aimed at graduate students in algebra and related topics at Edinburgh, Heriot-Watt and Glasgow universities. Aimed to approach Lean as mathematicians and future formalisers, establishing proficiency in tactic mode. For the first part of the course we learned the basics of first-order logic in Lean using the tutorials project, before discussing some basics of types and type classes to talk about formalising algebra. Also made use of lftcm2020 exercise sheets, and MiL. Concluded with a hackathon working on some group projects.

`, website: "https://www.maths.ed.ac.uk/~pkinnear/leancourse/", material: "None", repository: "None", notes: `None`, experiences: `

We tried to avoid touching on too much type theory early on to get people confidently interacting with Lean quickly. In retrospect, it would have been good to cover this in more depth (albeit only later in the course, after establishing confidence interacting with Lean) to aid in dealing with the inevitable issues that arise when formalising an interesting piece of mathematics. Also, we originally aimed for the outcome of the course to be group projects working on mathlib contributions, but would now say that re-framing the goal as formalising something new in a format that is useful to you as a learner (e.g. as a worksheet/interactive part of a textbook) is a better goal pedagogically (and could still lead to, e.g., a mathlib contribution in the process even if that isn't the explicit goal).

` }, - 16: { summary: `

This course introduces computer science students to propositional logic, predicate logic and modal logic. The course uses two formal proof systems: natural deduction (exam) and Lean (homework assignments).

+ 18: { summary: `

This course introduces computer science students to propositional logic, predicate logic and modal logic. The course uses two formal proof systems: natural deduction (exam) and Lean (homework assignments).

`, website: "https://studiegids.vu.nl/en/2022-2023/courses/X_401015", material: "https://leanprover.github.io/logic_and_proof/logic_and_proof.pdf", repository: "None", notes: `None`, experiences: `None` }, - 17: { summary: `

Since January 2019, I am using Lean to teach first year undergrad double major maths/CS students how to find and write mathematical proofs. I first did it alone and then with Frédéric Bourgeois and Christine Paulin. The main mathematical topic of this course is elementary real analysis, especially the theory of convergent sequences and continuous functions. Since 2021 I use a controlled natural language for input in order to facilitate transferring Lean proofs to pen and paper proofs.

+ 19: { summary: `

Since January 2019, I am using Lean to teach first year undergrad double major maths/CS students how to find and write mathematical proofs. I first did it alone and then with Frédéric Bourgeois and Christine Paulin. The main mathematical topic of this course is elementary real analysis, especially the theory of convergent sequences and continuous functions. Since 2021 I use a controlled natural language for input in order to facilitate transferring Lean proofs to pen and paper proofs.

`, website: "https://www.imo.universite-paris-saclay.fr/~patrick.massot/enseignement/", material: "None", repository: "https://github.com/PatrickMassot/MDD154/", notes: `