News SETI.Germany : LODA: 150000. Programm entdeckt und weitere Fortschritte

[P3D-Bot]

Das Projekt erreichte vor wenigen Wochen den Meilenstein von 150 000 entdeckten Programmen zur Erzeugung von ganzzahligen Folgen. Zu diesem Anlass wurden die Fortschritte seit dem letzten Meilenstein im Oktober 2025 zusammengefasst, darunter die Möglichkeit, die entdeckten Programme mit dem Beweisassistenten LEAN zu überprüfen.

Meilenstein von 150 000 Programmen erreicht
Wir freuen uns riesig bekanntzugeben, dass das BOINC-Projekt LODA einen weiteren beachtlichen Meilenstein erreicht hat: mehr als 150 000 entdeckte Programme! Dies bedeutet eine Steigerung um 10 000 Programme seit unserer letzten Mitteilung im Oktober 2025 und wir hätten dies nicht ohne eure engagierte Unterstützung und Rechenleistung erreichen können.

Größere Entwicklungen seit Oktober 2025

Eingebauter LEAN-Beweisassistent
Der wesentlichste Fortschritt war unsere umfassende Fähigkeit zur LEAN-Formelgenerierung. LODA kann nun Programme automatisch im LEAN-Format exportieren, was die formale Bestätigung von Formen für ganzzahlige Folgen ermöglicht. Diese bahnbrechende Funktion beinhaltet:

• Unterstützung für einfache rekursive Funktionen und mehrere wechselseitig rekursive Funktionen
• Unterstützung für die Operationen Fakultät (fac), Potenzieren (pow), Binomialkoeffizienten (bin) sowie bitweise Operationen
• LEAN-Unterstützung für automatisierte Tests und Bestätigungen

Diese Integration schlägt eine Brücke zwischen automatisierter Entdeckung von Programmen und formalem mathematischen Beweis und eröffnet neue Möglichkeiten für bestätigte Mathematik in der OEIS-Gemeinschaft.

Erweiterte Formelgenerierung
Wir haben die Möglichkeiten der Formelgenerierung dramatisch verbessert und unterstützen jetzt weitere LODA-Operationen, darunter Speicheroperationen (fil, rol, ror), bedingte Division (dif), digitale Wurzel (dir) und höchster Exponent (lex). Leistungsoptimierungen haben die Formelgenerierung signifikant beschleunigt.

Modernisierte Infrastruktur
Wir haben die Bibliotheken libcurl und zlib direkt in LODA eingebaut und somit die Abhängigkeit von den externen Programmen curl/wget und gzip/gunzip eliminiert. Dies macht LODA stärker in sich geschlossen und zuverlässiger auf allen Plattformen. Wir haben außerdem auf v2-API-Endpunkte umgestellt und das automatische Erkennen und Melden kaputter b-Dateien eingebaut, um die Datenqualität zu verbessern.

Unterstützte Plattformen
LODA unterstützt jetzt die Windows-ARM64-Architektur, was unsere Reichweite um neuere Windows-Geräte mit ARM-Prozessoren erweitert.

Verbesserte Leistung
Zahlreiche Optimierungen wurden implementiert, darunter verbessertes Verschmelzen von Operationen im Optimierer, besserer Umgang mit den Operationen pow und nrt sowie eine Vergrößerung des standardmäßigen Maximums des physischen Speichers, um mit größeren Rechenaufgaben umgehen zu können.

Ausblick
Mit nun mehr als 150 000 Programmen in unserer Datenbank verschiebt LODA weiterhin die Grenzen automatisierter mathematischer Entdeckungen. Die LEAN-Integration stellt einen wesentlichen Schritt hin zu formal bestätigten Programmen dar und wir sind gespannt zu sehen, wie diese Fähigkeit von der mathematischen Gemeinschaft genutzt werden wird.

Danke für eure unerschütterliche Unterstützung und für das Beitragen eurer Rechenleistung zur Erweiterung mathematischen Wissens. Jedes Programm, zu dessen Entdeckung ihr beitragt, bringt uns dem Verständnis der wunderschönen Muster näher, die in ganzzahligen Folgen verborgen sind!
14.02.2026, 19:39:44 MEZ

Originaltext:

Zitat von

150,000 Programs Milestone Reached

150,000 Programs Milestone Reached
We are thrilled to announce that the LODA BOINC project has reached another remarkable milestone: over 150,000 programs discovered! This represents a 10,000 program increase since our last announcement in October 2025, and we couldn't have achieved this without your dedicated support and computing power.

Major Developments Since October 2025

LEAN Theorem Prover Integration
The most significant advancement has been our comprehensive LEAN formula generation capability. LODA can now automatically export programs to LEAN format, enabling formal verification of integer sequence formulas. This groundbreaking feature includes:
* Support for simple recursive functions and multiple mutually recursive functions
* Support for factorial (fac), power (pow), binomial coefficients (bin), and bitwise operations
* LEAN project support for automated testing and validation
This integration bridges the gap between automated program discovery and formal mathematical proof, opening new possibilities for verified mathematics in the OEIS community.

Formula Generation Enhancements
We've dramatically improved formula generation capabilities, supporting more LODA operations including memory operations (fil, rol, ror), conditional division (dif), digital root (dir), and largest exponent (lex). Performance optimizations have made formula generation significantly faster.

Infrastructure Modernization
We've integrated libcurl and zlib libraries directly into LODA, eliminating dependencies on external curl/wget and gzip/gunzip tools. This makes LODA more self-contained and reliable across all platforms. We've also migrated to v2 API endpoints and added automatic detection and reporting of broken b-files for improved data quality.

Platform Support
LODA now supports Windows ARM64 architecture, expanding our reach to newer Windows devices with ARM processors.

Performance Improvements
Numerous optimizations have been implemented, including improved operation merging in the optimizer, better handling of pow and nrt operations, and increased default maximum physical memory for handling larger computation tasks.

Looking Forward
With over 150,000 programs now in our database, LODA continues to expand the boundaries of automated mathematical discovery. The LEAN integration represents a major step toward formally verified programs, and we're excited to see how this capability will be used by the mathematical community.

Thank you for your unwavering support and for contributing your computing resources to advance mathematical knowledge. Every program you help discover brings us closer to understanding the beautiful patterns hidden within integer sequences!
14 Feb 2026, 18:39:44 UTC

Lese weiter bei SETI.Germany....