Booth Demo Schedule
We're at MPI's booth 502
Tuesday, March 17th
2pm–2:30pm
Meet Ax-Measure, Axiomatic AI's testing solution for photonic integrated circuits
Wednesday, March 18th
11am–11:30am
Meet Ax-Measure, Axiomatic AI's testing solution for photonic integrated circuits
Watch
Can't make our live demos? Learn more about Axiomatic AI here.
Formalization with Lemma
Read
Explore our latest publications and papers.
Compact Modeling and Fitting of a CWDM Lattice-Filter Device: Interactive Digital Twin for Silicon Photonic MZI Arrays
Real-time Interactive Model Based on Cascaded Mach-Zehnder Interferometer Theory
A Minimal Agent for Automated Theorem Proving
Proposing a minimal agentic baseline that enables systematic comparison across different AI-based theorem prover architectures
Try
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 _)