Claude Code gives a model a shell and dev tools so it can write and run code. Bourbaki does the same for mathematics: a computer algebra system (SymPy), a proof assistant (Lean 4), and research APIs (OEIS, arXiv).
You ask in the TUI. The agent reasons, computes, verifies, looks things up, and streams the answer back.
If it writes a proof, it can formalize it. If it makes a claim, it can check it. That last sentence is the entire reason this exists.