diff --git a/100.html b/100.html index 068b2e22d0..70dcfdde16 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

@@ -401,7 +401,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

@@ -434,7 +434,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

@@ -459,7 +459,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

@@ -485,7 +485,7 @@
35. Taylor’s Theorem (hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Set.Icc x₀ x)) (Set.Ioo x₀ x)) :
∃ (x' : ℝ) (_ : x' ∈ Set.Ioo x₀ x), 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 @@ -504,7 +504,7 @@
35. Taylor’s Theorem (hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Set.Icc x₀ x)) (Set.Ioo x₀ x)) :
∃ (x' : ℝ) (_ : x' ∈ Set.Ioo x₀ x), 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

@@ -543,7 +543,7 @@
38. Arithmetic Mean/Geometric Mean (hz : ∀ 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

@@ -564,7 +564,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 @@ -574,7 +574,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.

@@ -617,7 +617,7 @@
40. Minkowski’s Fundamental Theorem (h : ↑↑μ F * 2 ^ FiniteDimensional.finrank ℝ E < ↑↑μ s) :
∃ (x : ↥L) (_ : x ≠ 0), ↑x ∈ s
-

docs, source

+

docs, source

@@ -645,7 +645,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

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

docs, source

+

docs, source

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

docs, source

+

docs, source

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

docs, source

+

docs, source

@@ -751,7 +751,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

@@ -775,7 +775,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 @@ -787,7 +787,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

@@ -826,7 +826,7 @@
59. The Laws of Large Numbers :
∀ᵐ (ω : Ω), 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

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

docs, source

+

docs, source

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

docs, source

+

docs, source

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

docs, source

+

docs, source

@@ -915,7 +915,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

@@ -946,7 +946,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

@@ -971,7 +971,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 @@ -979,7 +979,7 @@
66. Sum of a Geometric Series (hr : r < 1) :
HasSum (fun (n : ℕ) => r ^ n) (1 - r)⁻¹
-

docs, source

+

docs, source

@@ -999,7 +999,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

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

docs, source

+

docs, source

theorem EuclideanDomain.gcd_dvd @@ -1034,7 +1034,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 @@ -1050,7 +1050,7 @@
69. Greatest Common Divisor Algorithm {c : R} :
c ∣ a → c ∣ b → c ∣ EuclideanDomain.gcd a b
-

docs, source

+

docs, source

@@ -1078,7 +1078,7 @@
71. Order of a Subgroup [Fintype ↥s] :
Fintype.card ↥s ∣ Fintype.card α
-

docs, source

+

docs, source

@@ -1103,7 +1103,7 @@
72. Sylow’s Theorem (hdvd : p ^ n ∣ Fintype.card G) :
∃ (K : Subgroup G), Fintype.card ↥K = p ^ n
-

docs, source

+

docs, source

sylow_conjugate

card_sylow_dvd

card_sylow_modeq_one

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

docs, source

+

docs, source

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

docs, source

+

docs, source

theorem hasSum_fourier_series_L2 @@ -1179,7 +1179,7 @@
76. Fourier Series (f : ↥(MeasureTheory.Lp ℂ 2)) :
HasSum (fun (i : ℤ) => fourierCoeff (↑↑f) i • fourierLp 2 i) f
-

docs, source

+

docs, source

@@ -1194,7 +1194,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 @@ -1202,7 +1202,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

@@ -1227,7 +1227,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 @@ -1245,7 +1245,7 @@
78. The Cauchy-Schwarz Inequality (y : E) :
‖inner x y‖ ≤ ‖x‖ * ‖y‖
-

docs, source

+

docs, source

@@ -1284,7 +1284,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

@@ -1303,11 +1303,11 @@
80. The Fundamental Theorem of Arithme (h₂ : ∀ 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 @@ -1315,7 +1315,7 @@
80. The Fundamental Theorem of Arithme [EuclideanDomain R] :
IsPrincipalIdealRing R
-

docs, source

+

docs, source

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

docs, source

+

docs, source

theorem UniqueFactorizationMonoid.factors_unique @@ -1345,7 +1345,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.

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

docs, source

+

docs, source

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

docs, source

+

docs, source

@@ -1409,13 +1409,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

@@ -1434,7 +1434,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 @@ -1446,7 +1446,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

@@ -1457,7 +1457,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

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

docs, source

+

docs, source

@@ -1512,7 +1512,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

@@ -1551,7 +1551,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

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

docs, source

+

docs, source

@@ -1598,7 +1598,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 3d3d2eb44d..cbf14d5c1c 100644 --- a/mathlib_stats.html +++ b/mathlib_stats.html @@ -60,8 +60,8 @@

Counts

Contributors - 71928 - 129629 + 71981 + 129803 310 diff --git a/teaching/courses.html b/teaching/courses.html index f6e1de30ac..1f08d24a41 100644 --- a/teaching/courses.html +++ b/teaching/courses.html @@ -85,6 +85,8 @@

Courses using Lean

Czech +English + French German @@ -95,6 +97,8 @@

Courses using Lean

automated reasoning +beginner + computer science functional programming @@ -215,26 +219,30 @@

Courses using Lean

- Peter PfaffelhuberSome high-school mathematics in LeanUniversity of Freiburg, Germany2023German, intro to proof, mathematics, lean3 + Marc Masdeu, Roberto RubioPoden els ordinadors entendre les matemàtiques? De la geometria axiomàtica als theorem proversUniversitat Autònoma de Barcelona2023Catalan, English, beginner, mathematics, lean3 - Miguel MarcoTopología generalUniversidad de Zaragoza2023Spanish, 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 MarcoTopologí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 @@ -453,24 +461,28 @@
Contributing
`, experiences: `

This course really works well, and it will probably continue for a long time. The idea to use controlled natural language tactics seems a lot more efficient than the native syntax to ensure students improve at pen and paper proofs.

` }, - 24: { summary: `

The aim of the course is to learn some Lean 3 using easy mathemtics (such as divisibility, \sqrt 2 \notin \Q, and the pigeonwhole principle). The course is in German and was taught in summer 2023 for one full semester with weekly homeworks. We met once a week, discussed upcoming topics and started to work on the next exercises in class. The manuscript contains an extended cheat sheet for Lean tactics.

+ 24: { summary: `

This was a week-long (20h) summer course introducing motivated high school students to formal mathematics. Half of the time was spent teaching on a blackboard Hilbert's axioms for plane geometry, while the other half was spent on a computer lab playing through several levels of a Lean game whose ultimate goal was to proof the plane separation theorem. This was the first experience for the students with both axiomatic mathematics and theorem provers. While the course was taught in Catalan, the game is written in English.

+`, website: "https://mat.uab.cat/~masdeu/argo/", material: "None", repository: "https://github.com/mmasdeu/argo", notes: `None`, experiences: `

The students found the Lean part the most challenging part of the course. The students would happily seat through the traditional-style lecture, but struggled when they had to code in Lean the proofs that they had previously discussed. This is in part because of Lean's unforgiveness, but we believe it is also due to the fact that they were unaware of some misunderstandings about the proofs, and Lean made those emerge.

+` }, + + 25: { summary: `

The aim of the course is to learn some Lean 3 using easy mathemtics (such as divisibility, \sqrt 2 \notin \Q, and the pigeonwhole principle). The course is in German and was taught in summer 2023 for one full semester with weekly homeworks. We met once a week, discussed upcoming topics and started to work on the next exercises in class. The manuscript contains an extended cheat sheet for Lean tactics.

`, website: "https://github.com/pfaffelh/schulmathematik_mit_lean/", material: "https://github.com/pfaffelh/schulmathematik_mit_lean/blob/master/Manuskript/skript.pdf", repository: "None", notes: `None`, experiences: `

The course was intended for students in mathematics who want to become teachers, but was also taken by other math students. Only using Prop-types in the first few lessons was a good idea, in my opinion. The students liked the interactive feeling even of the simple proofs. Weekly homeworks were made quite consistently, the dropout-rate (among ~15 students) was low.

` }, - 25: { summary: `

It is a standard course on general topology in the Mathematics degree. It is taught in spanish, so the material in the repo uses spanish too. It is not a course about Lean: Lean is only used as a complement, to help students grab the steps of rigourous proofs. The usage of Lean is totally optional for the students.

+ 26: { summary: `

It is a standard course on general topology in the Mathematics degree. It is taught in spanish, so the material in the repo uses spanish too. It is not a course about Lean: Lean is only used as a complement, to help students grab the steps of rigourous proofs. The usage of Lean is totally optional for the students.

`, website: "https://sia.unizar.es/doa/consultaPublica/look[conpub]MostrarPubGuiaDocAs?entradaPublica=true&idiomaPais=es.ES&_anoAcademico=2023&_codAsignatura=27008", material: "None", repository: "https://github.com/miguelmarco/topologia_general_lean", notes: `None`, experiences: `

The course is still ongoing, so we still don't have evidence of success. We decided to use Lean3 instead of Lean4 because of the easyness to install the trylean bundle, but will reconsider this decision next year. Students seem to be uninterested and/or scared at the beginning, but as i had shown how to use it to prove some example exercises, some have shown more interest. We plan to do an introductory seminar for those that want to learn how to use it.

` }, - 26: { summary: `

This was taught as a third-year undergraduate course. We spent a little more than half the semester working through the first 6 chapters of Mathematics in Lean with weekly homework assignments. Students did a small independent project at the halfway point, and a larger one at the end.

+ 27: { summary: `

This was taught as a third-year undergraduate course. We spent a little more than half the semester working through the first 6 chapters of Mathematics in Lean with weekly homework assignments. Students did a small independent project at the halfway point, and a larger one at the end.

`, website: "None", material: "https://leanprover-community.github.io/mathematics_in_lean/mathematics_in_lean.pdf", repository: "https://github.com/leanprover-community/mathematics_in_lean", notes: `None`, experiences: `None` }, - 27: { summary: `

An Introduction To Proofs course at Johns Hopkins in Fall 2022 entirely in Lean (teaching and assessment) culminating in the proof of Yoneda Lemma.

+ 28: { summary: `

An Introduction To Proofs course at Johns Hopkins in Fall 2022 entirely in Lean (teaching and assessment) culminating in the proof of Yoneda Lemma.

`, website: "https://sinhp.github.io/teaching/2022-introduction-to-proofs-with-Lean", material: "None", repository: "https://github.com/sinhp/ProofLab", notes: `None`, experiences: `None` }, - 28: { summary: `

This is a game-based introduction to undergraduate pure mathematics, starting with equations, natural numbers, logic, sets, function, real numbers and sequences with draft sections on groups. A book is being written to accompany the game. The next iteration of the game will be in Lean 4.

+ 29: { summary: `

This is a game-based introduction to undergraduate pure mathematics, starting with equations, natural numbers, logic, sets, function, real numbers and sequences with draft sections on groups. A book is being written to accompany the game. The next iteration of the game will be in Lean 4.

`, website: "https://gihanmarasingha.github.io/modern-maths-pages/", material: "None", repository: "None", notes: `None`, experiences: `None` }, - 29: { summary: `

This is an introduction to logic and mathematical reasoning for a general audience. It was taught in the philosophy department at CMU twice.

+ 30: { summary: `

This is an introduction to logic and mathematical reasoning for a general audience. It was taught in the philosophy department at CMU twice.

`, website: "None", material: "https://leanprover.github.io/logic_and_proof/", repository: "None", notes: `None`, experiences: `None` }, };