Fuse is a desktop workspace for turning mathematical ideas into Lean proofs with Claude Code or Codex. Work with your LaTeX blueprint, Lean code, and AI agent in one place, using files in your own repository.
- Read and edit your blueprint, with a graph of how its definitions and theorems depend on each other.
- Write Lean proofs with live goals, diagnostics, and build results.
- Ask an agent to help formalize statements and prove lemmas.
- Review the agent’s changes and commit them with Git.
Install Node.js 22.12+ and Git, then run:
git clone https://github.com/project-numina/fuse-desktop.git
cd fuse-desktop
make appThis installs dependencies and opens Fuse. Run make app again to reopen it;
dependencies are reinstalled only when the dependency manifests change. Keep the
terminal open while using Fuse; press Ctrl+C to stop it.
On Windows, or if make isn't installed, run npm ci followed by npm run dev instead.
To use an agent, install and sign in to Claude Code or Codex. For Lean projects, install elan to manage your Lean toolchains.
Once Fuse opens:
- Open a folder containing your project, or open
fixtures/sample-blueprintto try the included example. - Create a workspace and choose its blueprint source and Lean project.
- Open the blueprint or a Lean file, and start a chat with your agent.
Use Help → Guide for a walkthrough and troubleshooting.
Fuse edits your project files in place and saves its settings and chat data locally. When you use an agent, prompts and relevant project content are sent to its model provider. You use your own agent account and can choose permissions in Settings.
See CONTRIBUTING.md for code and testing conventions, and the developer reference for architecture, builds, and releases. Report bugs through GitHub Issues; report security issues privately.