Formalising the Kruskal-Katona theorem in Lean

DOI10.1007/978-3-031-16681-5_5OpenAlexW4296050175MaRDI QIDQ6159369

Bhavik Mehta

Publication date: 2 June 2023

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-031-16681-5_5

zbMATH Keywords

extremal combinatoricsformalisationLean theorem prover

Mathematics Subject Classification ID

Computer science support for mathematical research and practice (68Vxx)

Cites Work

• Problems and results in extremal combinatorics. III.
• Compressions and isoperimetric inequalities
• Logarithmic order of free distributive lattice
• Formalizing Frankl’s Conjecture: FC-Families
• INTERSECTION THEOREMS FOR SYSTEMS OF FINITE SETS
• The Lean Theorem Prover (System Description)
• Extremal Problems for Finite Sets
• On generalized graphs
• A short proof of Sperner's lemma
• Generalization of Sperner’s Theorem on the Number of Subsets of a Finite Set
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Formalising the Kruskal-Katona theorem in Lean