Diferenciální geometrie představuje oblast matematiky kombinující diferenciální počet, topologii a algebru k popisu geometrických objektů. Jedním z těch nejdůležitějších jsou hladké distribuce. Existují kritéria pro jejich integrabilitu, Frobeniova a Štefanova-Sussmannova věta.
Úkolem studenta bude seznámit se se základními pojmy teorie hladkých distribucí a podrobně analyzovat tvrzení a důkazy obou zmíněných vět. Hlavní myšlenkou této bakalářské práce je vytvořit si matematické základy pro navazující úkol – počítačovou formalizaci Frobeniovy a Štefanovy-Sussmannovy pomocí asistenta důkazu Lean.
Počítačová formalizace a počítačové ověřování matematických definic, vět a důkazů je rychle se rozvíjející oblastí výzkumné matematiky. Jejím úkolem je převést základní matematické výsledky do jazyka srozumitelnému počítači. To umožní jejich algoritmické ověření a vytvoření knihovny formalizované matematiky. Ta by mohla v budoucnu sloužit například k učení velkých jazykových modelů.