Mathematics and physics are evolving disciplines. AI is increasingly becoming an active participant in that evolution, producing results at a speed and scale that are difficult to follow without appropriate computational tools.

In the ExaktAI project we are addressing two related issues: the reliability problem of AI mathematics through computational validation, and maximizing human participation in checking, understanding and extending the results.

For the latter, we developed the ExaktAI Workspace.

The Workspace is a full computational-mathematics document environment in which one can follow, inspect, modify and extend AI-generated mathematics, or simply do the mathematics directly. Of particular relevance here, the Workspace can run Maple directly when Maple is installed.

The public beta is now open. I would be particularly interested in feedback and suggestions, both about the Maple integration and about the broader ideas for keeping us, the humans, actively involved and increasingly participating in AI-mathematics developments.

Update, September 27: the Workspace now also provides a document interface for Lean, the theorem prover, with CAS computations inside proofs; see "The Lean theorem prover" below.

Edgardo S. Cheb-Terrab
ExaktAI, Canada
Research Fellow Emeritus at Maplesoft.

I am delighted to share that the ExaktAI Workspace now also provides a full-featured mathematical document interface for Lean, the theorem prover and proof assistant, integrated directly with computer algebra system (CAS) computation.

The Workspace, including its Lean integration, is in free beta testing and open to everybody.

Lean files (.lean) open as Lean documents, proofs are checked step by step with goals shown under each step, CAS computations can be inserted inside proofs, and a class of CAS results can be turned into Lean theorem candidates that Lean then independently checks.

The Workspace also includes a Lean tutorial, intended to make this accessible to users who are not yet familiar with Lean syntax and workflow.

CAS computations can be inserted between Lean proof steps. A class of CAS results can also be turned into Lean theorem candidates that Lean independently checks.



Edgardo S. Cheb-Terrab
ExaktAI, Canada
Research Fellow Emeritus at Maplesoft.