LODA: News https://boinc.loda-lang.org/loda/ LODA Language Sat, 14 Feb 2026 18:39:44 GMT en-us https://boinc.loda-lang.org/loda/rss_image.gif https://boinc.loda-lang.org/loda/ https://boinc.loda-lang.org/loda/forum_thread.php?id=139 https://boinc.loda-lang.org/loda/forum_thread.php?id=139
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! ]]> Sat, 14 Feb 2026 18:39:44 GMT