MOTO is an automated theorem generator for science. It's a creative novelty-seeking researcher with autonomous Lean 4 proof generation. Run for days at a time once pressing start - no interaction needed! Agents working in parallel from either local host LM studio, OpenRouter, OAuth or all 3. No internet required. Star us for more!

CLI tool for automated discovery of BPS models from event logs

Automatic discovery of non-trivial statistical truths from 500+ public time series — mutual information, Granger causality, FDR correction

Using AI to discover better evolutionary algorithms through automated code evolution with ShinkaEvolve

A propose → verify → evolve loop for exact solutions of Einstein's field equations — genetic programming proposes, SymPy proves (theorem or nothing). Also: proven Kaluza–Klein/thermodynamic-gravity theorems, chaos as a LISA signature, and the first Python Cartan–Karlhede equivalence-problem solver.

Discover statistically significant lagged relationships in public time series data with automated multi-stage validation and noise filtering