LODA

LODA BOINC
Project
Status	Completed
Category	Mathematics
Compute	CPU
Requires	Git
Development
Developer	LODA Language contributors
Maintainer	LODA Language project
Initial release	2022-05-13
Completed	2026-09-10
Repository	https://github.com/loda-lang
Software
Written in	C++, Rust, LODA
Operating system	Windows 10 or higher, Linux, macOS
Metadata
Website	https://boinc.loda-lang.org/loda/
License	Open source

LODA BOINC was a volunteer computing project based on the Berkeley Open Infrastructure for Network Computing (BOINC) platform. It used computing resources donated by volunteers to search for programs, formulas, and algorithms for integer sequences in the On-Line Encyclopedia of Integer Sequences (OEIS).

LODA BOINC was part of the wider LODA Language project. LODA is an assembly language, a computational model, and a set of tools for the automated discovery and analysis of programs that calculate integer sequences. The project combined a specialized programming language with program mining software and a public database of mined programs.

For a sequence represented by terms such as $a_0,a_1,a_2,\dots$, the purpose of a LODA program was to calculate the corresponding value $a_n$ from an input index $n$. Program mining attempted to discover short or efficient algorithms that reproduced known sequence terms and could be tested against OEIS data.

The BOINC project began operating in May 2022. Its launch announcement invited volunteers to contribute computing power to the search for new programs for integer sequences. The project was shut down on 10 September 2026. The shutdown was announced in a project news post that stated that recent advances in artificial intelligence had made AI-based methods increasingly effective for program and formula discovery.

The original project website was unavailable when this article was updated. A Wayback Machine capture made on 21 September 2026 preserves the project homepage, its description of the research goal, its operating system requirements, and the shutdown announcement.

Name and purpose

LODA stands for Lexicographical Order Descent Assembly. The name refers to the language's use of a lexicographical descent condition in its loop construct. LODA programs operate on integer memory cells and use arithmetic and number-theoretic operations to calculate sequence values.

The LODA project focused on integer sequences rather than on a single scientific field such as astronomy, climate modelling, or molecular biology. Its principal source of target sequences was the OEIS, a database containing information about integer sequences and their mathematical properties. The purpose of program mining was to find executable descriptions of sequences for which no short or efficient algorithm was known, or to find shorter and faster alternatives to existing descriptions.

A mined LODA program was not necessarily presented as a conventional mathematical formula. It was an executable algorithm that could be tested against the known terms of an OEIS sequence. Some programs could subsequently be converted into formulas or exported to other mathematical systems for further analysis.

For example, an OEIS sequence can be viewed as a function

$f:\mathbb{\mathbb{N}}\to \mathbb{\mathbb{Z}}$

where the input $n$ is a non-negative integer and the output $f(n)$ is the corresponding sequence term. LODA programs were designed to express such functions using compact arithmetic instructions and reusable sequence programs.

Program mining

Program mining is the automated process of searching for programs that calculate desired outputs. In the LODA project, the search began with integer sequences and attempted to construct short programs that reproduced their terms. The LODA documentation describes the project as supporting the discovery, execution, optimization, and analysis of programs for integer sequences.

The mining process could produce candidate programs and then test them against sequence data. Programs could be optimized, checked, minimized, and exported in different formats. The command-line implementation included separate commands for evaluating programs, checking them, mining new programs, submitting programs, optimizing programs, and converting programs into other representations.

A candidate program was evaluated at one or more input values. If a program $P$ was intended to calculate a sequence $a_n$, the result could be compared with the corresponding OEIS terms:

$P(n)=a_n$

The comparison could be repeated over a range of values of $n$. Matching known terms did not by itself constitute a mathematical proof for every possible input, but it provided a computational test for a candidate program.

The project described its search methods as including evolutionary algorithms and machine learning techniques. These methods were used to explore possible programs and to improve candidate solutions according to criteria such as correctness, program length, and execution efficiency.

The use of distributed computing was motivated by the large search space involved in program discovery. A volunteer computer could run mining tasks in the background and return results to the project. The BOINC infrastructure handled the distribution of work and the collection of results, while the LODA software performed the sequence-program search.

A simplified description of the search process is:

$\text{candidate program}⟶\text{execution}⟶\text{comparison with sequence data}⟶\text{optimization or rejection}$

The actual mining system used project software and configuration files rather than this simplified mathematical description.

LODA language

The LODA language is an assembly-like language designed for arithmetic and number-theoretic computation. It does not use named variables in the usual programming-language sense. Instead, programs use an unbounded set of integer memory cells, represented by numbered locations such as $0, $1, and $2.

The memory model can be described mathematically as a sequence of integer cells:

$m_0,m_1,m_2,\dots \in \mathbb{\mathbb{Z}}$

The cells are mutable during program execution. A LODA instruction can read values from memory cells, perform an arithmetic operation, and write a result to a memory cell.

For programs that calculate integer sequences, memory cell $0 is used to pass the input argument and store the result. Other memory cells can be used for intermediate values. If the input is $n$, the program begins with the input represented in the primary memory cell and eventually returns a value intended to equal $a_n$.

This design allows programs to express arithmetic calculations and more complex algorithms using a compact instruction sequence. Since the language is designed around integer calculations, its operations are suited to the manipulation of sequence terms, indices, counters, and intermediate values.

A notable language feature is the seq operation, which permits one sequence program to use another sequence program. This allows programs to be composed from previously discovered building blocks. The resulting program can refer to other OEIS-related programs without reproducing all of their instructions directly.

If a program for sequence $b_n$ uses another program for sequence $a_n$, the composition can be represented conceptually as:

$b_n=g(a_n)$

The exact operations and syntax are defined by the LODA language specification. The expression above is only a mathematical illustration of how one program may use the result of another.

The language also includes a loop construct based on lexicographical descent. The specification describes the loop as operating while a vector of memory values remains non-negative and decreases according to lexicographical ordering.

A vector used by such a loop can be represented as:

$\mathbf{𝐯}=(m_i,m_{i+1},\dots ,m_j)$

The loop condition compares successive values of this vector using lexicographical order. This provides a mechanism for expressing iterative algorithms while retaining the mathematical structure associated with the LODA model.

Software implementation

The principal implementation described by the project was loda-cpp, a C++ implementation of the LODA language. The repository describes it as providing an interpreter, optimizer, formula generator, and miner. It can evaluate programs directly, verify programs against sequence data, and search for new programs.

The command-line tool supported single-core and parallel mining. It also included options for limiting execution time, the number of execution steps, memory use, and the number of mining hours. These options were useful for running the software in different environments, including volunteer computing applications with scheduled or limited processing time.

The mining commands could be used in single-process or parallel modes. In conceptual terms, parallel mining divided the search into multiple independent or partially independent searches:

$S=S_1\cup S_2\cup \cdots \cup S_k$

where $S$ represents the overall search space and each $S_i$ represents a portion explored by a mining process. The actual distribution of work was controlled by the LODA software and BOINC project infrastructure.

The wider LODA organization also maintained a Rust implementation and other repositories related to the web editor, API services, program data, and BOINC integration. The GitHub organization identifies repositories including loda-programs, loda-rust, loda-cpp, loda-api, and loda-boinc.

BOINC operation

LODA distributed mining work through BOINC. Volunteers installed the BOINC client, attached it to the LODA project, and contributed CPU time to the search for programs for integer sequences.

Before its shutdown, the project supported Windows 10 or higher, Linux, and macOS. The project also required the Git version control tool for its normal setup. Windows users were directed to Git for Windows, while Ubuntu and Debian users were directed to install Git through their package manager.

The archived project homepage instructed users to install Git before running LODA. The use of Git was connected with the project's method of distributing and updating LODA software, sequence data, and program repositories.

The project homepage also stated that volunteer contributions were acknowledged in the mined programs. This provided a way for participants to receive recognition for the computing resources they contributed to the project.

The BOINC project used CPU resources rather than presenting itself as a graphics processing unit project. The purpose of the contributed processing time was to execute mining tasks, evaluate candidate programs, and submit useful results to the project infrastructure.

Project results

In February 2026, the project announced that more than 150,000 programs had been discovered. The announcement described this as a milestone made possible by the computing power contributed by volunteers.

The same announcement described several developments in the LODA software. These included the ability to export programs to the LEAN theorem prover, support for simple recursive functions and mutually recursive functions, and support for operations such as factorials, powers, binomial coefficients, and bitwise operations.

The project also reported improvements to formula generation and support for additional operations, including memory operations, conditional division, digital roots, and largest-exponent calculations. The announcement further described infrastructure changes intended to reduce external dependencies and improve reliability across supported platforms.

The discovered programs were maintained in public repositories. The project homepage stated that volunteer contributions were acknowledged in the mined programs, and the shutdown announcement stated that the programs and results would remain available on GitHub.

The project output can be understood as a collection of program descriptions associated with sequence identifiers. In a simplified representation, a program database may be viewed as a set of pairs:

$\{(A_i,P_i)\}$

where $A_i$ is an OEIS sequence identifier and $P_i$ is a LODA program associated with that sequence. This representation is conceptual and does not describe the exact internal format of the project repositories.

Relation to formal mathematics

LODA programs provide executable descriptions of integer sequences. In some cases, an executable program can be transformed into a conventional formula or another representation that is easier to inspect mathematically. The LODA project website describes connections with computer algebra systems and theorem provers, including PARI/GP and LEAN.

The integration with LEAN described in the February 2026 milestone announcement was intended to support formal testing and validation of generated formulas. This did not mean that every program discovered by the BOINC project had been formally proved. Rather, it provided a route for selected programs and formulas to be translated into a theorem-proving environment for further verification.

The distinction between a program that reproduces known sequence terms and a formally verified mathematical result was important to the project. A program could be computationally tested against available OEIS data while still requiring additional mathematical analysis to establish a proof about all terms of a sequence.

For example, checking that a program produces the first several terms establishes a finite set of equalities:

$P(0)=a_0,P(1)=a_1,\dots ,P(k)=a_k$

A formal proof of correctness would generally require establishing the relationship for all relevant inputs:

$\mathrm{\forall }n\in \mathbb{\mathbb{N}},P(n)=a_n$

These two forms of validation are related but not identical.

Community and preservation

LODA BOINC was supported by volunteers within the wider BOINC community. The original project homepage provided a forum for help and discussion and directed users to the LODA Discord community.

The project also appeared in BOINC community discussions and was announced on Reddit when it began operating. The launch discussion described LODA as an assembly language, computational model, and distributed tool for mining programs for OEIS sequences. It also mentioned support for Windows, Linux, and macOS and the requirement to install Git.

Although the BOINC project ended in September 2026, the LODA Language project continued to provide source code and program data through GitHub. The shutdown announcement specifically stated that the LODA programs and results would remain accessible after the BOINC project ended.

The archived homepage provides historical information about the project that is no longer available from the live project website. It records the project's research goal, software requirements, links to project resources, volunteer recognition policy, and final news announcement.

The preservation of the source repositories and mined programs means that the end of the BOINC project did not necessarily end access to its computational output. The BOINC service ended, but the associated LODA software and program data remained part of the wider open-source project.

Shutdown

The shutdown was announced on 10 September 2026 in a news item titled "Shutdown of LODA BOINC". The project administrator wrote that distributed computing had been an effective way to search for LODA programs and mathematical solutions when the project began. The announcement stated that advances in artificial intelligence had changed the relative effectiveness of that approach.

The announcement thanked participants who had contributed computing power and support over the years. It also stated that the LODA programs and results would remain available through GitHub. The announcement was reproduced on the archived LODA homepage and was carried in the BOINC project news feed.

The project website was unavailable when this article was updated. The Wayback Machine capture from 21 September 2026 is therefore used as the principal source for the former homepage and its historical description of the project.

The reason given for the shutdown was a change in the relative usefulness of volunteer distributed computing for this particular research problem. The announcement did not state that the LODA language, repositories, or mined results had been abandoned. Instead, it stated that the existing programs and results would remain available through GitHub.

Timeline

Date	Event
13 May 2022	The project administrator announced that LODA was running on BOINC.
14 May 2022	A launch discussion was posted on the BOINC subreddit. It described LODA as an assembly language, a computational model, and a distributed tool for mining programs for integer sequences. The discussion also described the project's operating system and Git requirements.
14 February 2026	LODA BOINC announced that more than 150,000 programs had been discovered. The announcement also described LEAN integration and other software improvements.
10 September 2026	The project announced its shutdown.
21 September 2026	A Wayback Machine capture preserved the project homepage and the shutdown announcement after the project ended.

See also

• Volunteer computing
• BOINC
• On-Line Encyclopedia of Integer Sequences
• Automated theorem proving
• Program synthesis

External links

• https://github.com/loda-lang - LODA Language organization on GitHub
• https://github.com/loda-lang/loda-programs - LODA programs for integer sequences
• https://github.com/loda-lang/loda-cpp - LODA C++ implementation
• https://loda-lang.org/ - LODA Language website
• https://loda-lang.org/spec/ - LODA Language specification
• https://web.archive.org/web/20260921044946/https://boinc.loda-lang.org/loda/ - Archived LODA BOINC project homepage
• https://boinc.berkeley.edu/ - BOINC