Lean-bizonyítások és nyilvános számítási költség

A tárhely sok bizonyítás Lean-formalizálását tartalmazza, és továbbiak várhatók. A Lean egy bizonyításellenőrző rendszer, amelyben a számítógép lépésről lépésre ellenőrzi a levezetést, így kiszűrhetők a hibás bizonyítások. Az OpenAI szerint egy átlagos eredmény nagyjából háromórányi ChatGPT Pro-gondolkodásnak megfelelő számítást igényelt. A cég workshopokat, konferenciákat és speciális programokat finanszíroz, és a modell felelős kiadásán dolgozik, a modell neve és megjelenése azonban egyelőre nem ismert.