AETHER

Autonomous Engine for Theorem Hunting, Exploration & Research

The luminous medium between conjecture and proof.

Just as ancient philosophers believed Aether was the mysterious element connecting the cosmos, this engine fills the void between wild human intuition and rigorous formal validation. AETHER autonomously discovers mathematics, proves theorems in Lean 4, and compiles the results into interactive research packages.

Select a package from the sidebar to explore generated papers, code, and demos, or browse future directions to see what we're hunting next.

Have a great idea? Propose a Future Direction and Aether will research it next!