Booth Demo Schedule
We're at Hall 8.0, Stand 8.0D39.2
Monday, March 2nd
14:00–14:30
Meet Lemma, Your Co-Explorer for Science and Engineering
Tuesday, March 3rd
11:00–11:30
Lemma's Reasoning Engine
Tuesday, March 3rd
14:00–14:30
Reproduce, Refine, and Optimize with Lemma
Wednesday, March 4th
11:00–11:30
Meet Lemma, Your Co-Explorer for Science and Engineering
Wednesday, March 4th
13:30–14:00
Lemma's Knowledge Graph
Video Demos
Can't make our live demos? Watch Lemma in action here.
Formalization with Lemma
Try the Tools Behind our Demos
We've open-sourced AxProverBase, an automated theorem proving agent that is one of the core components of Lemma.
AxProverBase can be run locally, via MCP server, or as a GitHub integration.
$ ax-agent prove Topology/Basic.lean:compact_of_finite
Prebuilding Lean4 repo...
Proposing proof (iteration 1)
Running Lean compiler...
✗ Build failed: type mismatch, expected IsCompact
Proposing proof (iteration 2)
Refining with compiler feedback...
Running Lean compiler...
Build successful
Review: APPROVED ✓
✓ Proven (2 iterations, 14.2s)
theorem compact_of_finite
[TopologicalSpace α] [Finite α]
[DiscreteTopology α] :
IsCompact (Set.univ : Set α) :=
Set.Finite.isCompact (Set.toFinite _)