Advanced Search
All Posts : Applications, Examples and Libraries

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.
interface proof workspace lean

Please Wait...