b-mehta · July 1, 2020 19:47
diff --git a/BM projects b/BM projects
 Here's a quick list of things I'd like to see done in Lean, some of these could form good student projects depending on the student's background: They're a mix of category theory and combinatorics since those are the things I've done most in Lean. I'll add a disclaimer that there are people who believe category theory in Lean is hard for beginners, I disagree but of course your experience may differ from mine. An advantage of category theory in Lean though is that the Isabelle people are nowhere close to getting any, so you get to flex on them.
 - Adjoint functor theorems
  - For someone who's seen a small amount of category theory either of these should be pretty manageable: I don't think there are any steps of the proof which are particularly hard in Lean.
 - Enriched categories
  - Requires familiarity with category theory, some work has already been done in special cases by Scott Morrison and Markus Himmel, might be hard in Lean.
 - Filtered colimits (+commuting with finite limits in Set)
  - Requires familiarity with category theory.
 - If a functor preserves products and equalizers then it preserves limits.
  - I tried this and it's not the easiest, nor is it the most exciting but it's certainly doable.
 - Category theory game!
 - This theorem: https://github.com/b-mehta/topos/issues/3
 - Combinatorics game
 - Finite (hypergraph) Ramsey's theorem
  - I've done the non-hypergraph version and it was a bit unpleasant, but I think the general version might actually be easier (this is what I found for the infinite version).
 - Roth's theorem
  - This would be a super fun project, but might involve getting to grips with quite a lot of mathlib first, and you'll need to create lemmas for discrete Fourier transforms on an abelian group.
 - Szemeredi's Regularity Lemma
  - I think the hard part here is the algebraic steps - there are some numerical approximations which omega/linarith might struggle to do
 - Direct proofs of Erdos-Ko-Rado and Sperner's theorem
  - I have indirect proofs, but there are shorter proofs of both - I think in either case you'd need to know the list and finset APIs well, and possibly some induction. (Proving Bollobas two families might be nice too, as a generalisation of EKR).
 - Harper's theorem
  - I've done Kruskal-Katona with UV-compressions so the general proof idea for Harper by compressions is definitely doable
 - Bollobas-Thomason box theorem
  - Nice and self contained, but the induction step might be very tricky to figure out. A cool result though.
 - Categorical Ramsey theorems (I've already posted about this somewhere in the server)
	Here's a quick list of things I'd like to see done in Lean, some of these could form good student projects depending on the student's background: They're a mix of category theory and combinatorics since those are the things I've done most in Lean. I'll add a disclaimer that there are people who believe category theory in Lean is hard for beginners, I disagree but of course your experience may differ from mine. An advantage of category theory in Lean though is that the Isabelle people are nowhere close to getting any, so you get to flex on them.
	- Adjoint functor theorems
	- For someone who's seen a small amount of category theory either of these should be pretty manageable: I don't think there are any steps of the proof which are particularly hard in Lean.
	- Enriched categories
	- Requires familiarity with category theory, some work has already been done in special cases by Scott Morrison and Markus Himmel, might be hard in Lean.
	- Filtered colimits (+commuting with finite limits in Set)
	- Requires familiarity with category theory.
	- If a functor preserves products and equalizers then it preserves limits.
	- I tried this and it's not the easiest, nor is it the most exciting but it's certainly doable.
	- Category theory game!
	- This theorem: https://github.com/b-mehta/topos/issues/3
	- Combinatorics game
	- Finite (hypergraph) Ramsey's theorem
	- I've done the non-hypergraph version and it was a bit unpleasant, but I think the general version might actually be easier (this is what I found for the infinite version).
	- Roth's theorem
	- This would be a super fun project, but might involve getting to grips with quite a lot of mathlib first, and you'll need to create lemmas for discrete Fourier transforms on an abelian group.
	- Szemeredi's Regularity Lemma
	- I think the hard part here is the algebraic steps - there are some numerical approximations which omega/linarith might struggle to do
	- Direct proofs of Erdos-Ko-Rado and Sperner's theorem
	- I have indirect proofs, but there are shorter proofs of both - I think in either case you'd need to know the list and finset APIs well, and possibly some induction. (Proving Bollobas two families might be nice too, as a generalisation of EKR).
	- Harper's theorem
	- I've done Kruskal-Katona with UV-compressions so the general proof idea for Harper by compressions is definitely doable
	- Bollobas-Thomason box theorem
	- Nice and self contained, but the induction step might be very tricky to figure out. A cool result though.
	- Categorical Ramsey theorems (I've already posted about this somewhere in the server)