✦ logica lumina

Theorem Hearts

To cast is to prove; to prove is to heal.
Logic as spellcasting. Formal systems as enchantment.

Enter the Dream Source Code
"A bridge between the rigid world of logical proofs and the infinite truths of love."

Theorem Hearts is a custom C++ game engine where logic is the magic system. Magical girls wield spells powered by the Lean 4 theorem prover to solve puzzles, duel, and heal the world.

Each challenge is built from Lean modules. As players progress, puzzles adapt to their skill level, unlocking more sophisticated tactics. Deeply integrated. Formally verified. Currently dreaming.

Architecture

C++ Engine ↔ Lean Runtime
(Rendering / ECS)       (Proof Logic / Magic)

Linking Lean statically for smooth releases, with hot-swappable DLLs for development. A deterministic turn-based JRPG foundation powered by axiomatic truth.