Ebben a rövid bemutatókban élőben teszteljük a Gemini Pro-t. Két matematikai struktúrára (egy valószínűségelméletire és egy kategóriaelméletire) kérünk tőle Lean definíciókat, állításokat és bizonyításokat. Az AI által generált kódot validáljuk, az esetleges hibákat pedig iteratívan, a hibaüzenetek alapján kijavíttatjuk a Gemini-jal. Kitérünk a Coq Hammerre is, mint hatékony nem-statisztikai, automatizált Coq-beli bizonyításkeresőre ("no-brain" bizonyításokban elég jó ez is). Végül egy példán keresztül illusztráljuk a Lean egy hátrányát a Coq-kal szemben.