Ebben a tartalomban a Kimina prover nevű mesterséges intelligencia modellt mutatják be, amely kiemelkedő eredményeket ér el a matematikai tételbizonyításban. A bemutató során részletesen kitérnek arra, hogyan telepíthető és használható a modell helyileg, a Lean 4 nyelvi környezetben.
Felmerül a kérdés, vajon képes-e egy gépi tanuláson alapuló rendszer ugyanolyan módon gondolkodni, mint egy emberi matematikus. Ennek vizsgálata különböző matematikai problémák, például a háromszög belső szögeinek összege vagy a Cauchy–Schwarz-egyenlőség alapján történik.
Érdekes témakör még a mesterséges intelligencia által használt formális érvelési mintázat, amely hidat képez a formális verifikáció és az informális, emberi matematikai intuíció között. A néző betekintést kap a modell architektúrájába és teljesítményébe, valamint a különböző verziók sajátosságaiba.
További kérdéseket vet fel, hogy miként lehet optimalizálni a működést, például a paraméterek beállításával, illetve milyen feltételek szükségesek a hatékony használathoz – például a GPU-igények tekintetében.
