Willkommen @mathematics_inc - ein neues Unternehmen, das sich der Autoformalisierung und der Schaffung von verifizierter Superintelligenz widmet, die in den letzten Monaten bei Morph inkubiert wurde. Einzigartig ermöglicht durch die Infinibranch-native Umgebung von Morph, ist das erste Produkt von Math, Inc. Gauss, ein Autoformalisierungsagent, der eine beispiellose Skalierung der Rechenleistung zur Testzeit für dieses Gebiet erreicht, mit Tausenden von gleichzeitigen Agenten, die jeweils bis zu 12 Stunden am Stück arbeiten, um eine 25.000 LOC-Formalisierung des Strong Prime Number Theorem zu erstellen. Dies komprimiert, was früher Jahre für Experten in Anspruch nahm, auf nur wenige Wochen. Es ist ein Blick in die Zukunft der Wissensarbeit --- autonom, planetarisch skalierbar, entworfen, um Menschen und ihre glorreichen Errungenschaften zu ermächtigen --- die auf Morph Cloud aufgebaut wird.
Heute kündigen wir Gauss an, unseren ersten Autoformalisierungsagenten, der gerade das Projekt zum Starken Primzahlsatz von Terry Tao und Alex Kontorovich in 3 Wochen abgeschlossen hat – ein Aufwand, der menschlichen Experten über 18 Monate teilweise Fortschritt gekostet hat.
Wir freuen uns, @jdlichtman bei Morph als unseren Chefmathematiker willkommen zu heißen, wo er den Weg zur verifizierten Superintelligenz verkürzen wird.
Wir freuen uns, Trinity anzukündigen, ein Autoformalisierungssystem für verifizierte Superintelligenz, das wir bei @morph_labs entwickelt haben. Wir haben es verwendet, um ein klassisches Ergebnis von de Bruijn automatisch in Lean zu formalisieren, dass die abc-Vermutung fast immer wahr ist.