\n Formalization of a large number of definitions and theorems in Algebra, Number\n Theory and Analysis in\n the lean\n prover<\/a> brings the field of formal theorem proving to the forefront of\n mathematical research. However, mathematical notions and results from the\n field of Formal Concept Analysis are not yet included. Thus, the goal of this\n project (or thesis) is to formally prove the “Basic Theorem on Concept\n Lattices” (or a comparable result), in order to provide a stepping stone in\n this direction. Essentially, this involves building core definitions and\n necessary preliminary results\n by extending\n existing ones<\/a>. We will aim to build\n a lean blueprint<\/a>\n and if you are only interested in a small project, we will find a reasonable\n partial realization to stop at.\n<\/p>\n\n\n\n Inquiries: Tobias Hille<\/a><\/p>\n","protected":false},"excerpt":{"rendered":" Formalizing Results of Formal Concept Analysis Formalization of a large number of definitions and theorems in Algebra, Number Theory and Analysis in the lean prover brings the field of formal theorem proving to the forefront Read more…<\/a><\/p>\n","protected":false},"author":20,"featured_media":0,"comment_status":"closed","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"footnotes":""},"categories":[1,36,37,34,35],"tags":[57,66,56,65],"class_list":["post-9850","post","type-post","status-publish","format-standard","hentry","category-allgemein","category-bachelor","category-master","category-methodischer-schwerpunkt","category-technischer-schwerpunkt","tag-ss2025","tag-ss2026","tag-ws2024-25","tag-ws2025-26"],"translation":{"provider":"WPGlobus","version":"3.0.2","language":"en","enabled_languages":["de","en"],"languages":{"de":{"title":true,"content":true,"excerpt":false},"en":{"title":false,"content":false,"excerpt":false}}},"_links":{"self":[{"href":"https:\/\/www.kde.cs.uni-kassel.de\/en\/wp-json\/wp\/v2\/posts\/9850","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.kde.cs.uni-kassel.de\/en\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.kde.cs.uni-kassel.de\/en\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.kde.cs.uni-kassel.de\/en\/wp-json\/wp\/v2\/users\/20"}],"replies":[{"embeddable":true,"href":"https:\/\/www.kde.cs.uni-kassel.de\/en\/wp-json\/wp\/v2\/comments?post=9850"}],"version-history":[{"count":5,"href":"https:\/\/www.kde.cs.uni-kassel.de\/en\/wp-json\/wp\/v2\/posts\/9850\/revisions"}],"predecessor-version":[{"id":10326,"href":"https:\/\/www.kde.cs.uni-kassel.de\/en\/wp-json\/wp\/v2\/posts\/9850\/revisions\/10326"}],"wp:attachment":[{"href":"https:\/\/www.kde.cs.uni-kassel.de\/en\/wp-json\/wp\/v2\/media?parent=9850"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.kde.cs.uni-kassel.de\/en\/wp-json\/wp\/v2\/categories?post=9850"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.kde.cs.uni-kassel.de\/en\/wp-json\/wp\/v2\/tags?post=9850"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}