Tim Leanstral objavio je novu inačicu 1.5 modela s 6 milijardi aktivnih parametara, koja značajno unaprjeđuje formalnu verifikaciju. Model postiže vrhunske rezultate na FATE-H (87 posto) i FATE-X (34 posto), rješava 587 od 672 problema na PutnamBenchu te zasićuje miniF2F. Uz to, otkrio je pet ranije nepoznatih grešaka u 57 testiranih repozitorija.