https://en.wikipedia.org/wiki/Discrete_mathematics

# Graphs

See note on graphs

# Knots

https://en.wikipedia.org/wiki/Knot_polynomial

Rational Tangles - infinite series

# Matroids

https://en.wikipedia.org/wiki/Matroid

“where greedy works”

https://en.wikipedia.org/wiki/Submodular_set_function

greedoids

https://en.wikipedia.org/wiki/User:David_Eppstein/Matroid_Theory

# Packings

Circle packing. Really cool. A discrete analog of complex functions

# Combinatorics

Binomial

Shadow calculus Sums https://en.wikipedia.org/wiki/Umbral_calculus

Concrete mathematics

pigeon hole principle The continuous analog.

polya enumeration theorem polya’s theory of counting

handbook of combinatorics

https://en.wikipedia.org/wiki/Combinatorial_design

Finite geometry

https://en.wikipedia.org/wiki/Incidence_structure

# Ramsey Theory

Big step up in sophistication huh Principles that

Cody says has something to do with well quasi-orders

https://en.wikipedia.org/wiki/Schur%27s_theorem https://mathworld.wolfram.com/SchurNumber.html Schur number 5 = 161. 2017

Ramsey number solution to party problem. R(m,n) m know each other or n don’t know each other. Diagonal vs nondiagonal 2023 breakthrough on upper bound

# Logic

See lik the whole pile on logic

Ditto

# Order Theory

https://en.wikipedia.org/wiki/Order_theory

https://en.wikipedia.org/wiki/Dilworth%27s_theorem Finite po-sets

https://en.wikipedia.org/wiki/Hasse_diagram visualizing posets

https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Init/Order/Defs.lean

-- an attempt
class PartialOrder (A : Type) (R : A -> A -> Prop) where
refl : forall x, R x x
antisym : forall x y, R x y -> R y x -> x = y
trans : forall x y z, R x y -> R y z -> R x z

instance : PartialOrder Nat Eq where
refl := fun x => by rfl
antisym := fun x y r1 _r2 => by rw [r1]
trans := fun x y z r1 r2 => by rw [r1, r2]

def main := IO.println "hello world"