ExaktAI Workspace

Download

The Workspace is a computational environment where mathematical computing systems work together, even in a single document. Mathematics is the language: write in the SymPy, Maple, Mathematica or MATLAB dialect, and compute with the software you choose. SymPy, NumPy, SciPy and Matplotlib are included; Maple, Mathematica, MATLAB and Lean work alongside them when installed on your computer.

Symbolic and numerical computation, interactive plots, and proofs checked by Lean sit side by side, with a computation between two proof steps if you need one. Close the Workspace and open it again: every document is where you left it, the unsaved ones included. AI mathematics is here to stay, and the Workspace is where you can follow, reproduce, modify and extend it, or simply do the mathematics yourself.

The Workspace is free for everybody through June 30, 2027.

After June 30, 2027, using the Workspace with the SymPy, NumPy, SciPy and Matplotlib that come with it remains free for personal use, together with most of the Workspace's features. The free version includes computing mathematics written in SymPy as described on this page, and also includes working with mathematics written in Maple, Mathematica or MATLAB and computed with SymPy, NumPy and SciPy, where translation is possible and implemented. Opening Maple, Mathematica, MATLAB, Jupyter and Lean files also remains free, as do basic ExaktAI extensions such as the FunctionWizard. All Workspace features →

Universities, departments and companies can use the Workspace free through June 30, 2027. Institutional licences, now or for after that date, are arranged through info@exaktai.ai.

The Workspace

In the Workspace document, text, executable mathematical input, and results are interleaved. Results are typeset and numbered so they can be referenced in later computations. You can move freely through the document, revise any earlier computation, and run it again. Plots are interactive by default: you can zoom and pan them, or read a value off the curve. You can split the screen, keeping the upper pane in view while you write in the lower one. This is the full computer-algebra interface, familiar to users of Maple worksheets, Mathematica notebooks, and MATLAB Live Scripts. The interface comes in three themes, ExaktAI, Light, and Dark, and includes an AI assistant that opens in a separate window. The assistant can use your paid AI subscriptions or limited no-charge access to Gemini and Groq.

The ExaktAI Workspace includes SymPy, NumPy, SciPy and Matplotlib^*, and drives your own Maple, Mathematica or MATLAB, or the Wolfram Engine, which you can install free for non-commercial, personal use. For proofs, it drives Lean.

Dialect you write	SymPy	Maple	Mathematica	MATLAB
	Software that computes
SymPy	runs as written	translated	translated	translated
Maple	translated	runs as written	translated	translated
Mathematica	translated	translated	runs as written	translated
MATLAB	translated	translated	translated	runs as written

Every document has its dialect and its mathematical software, the engine, set, shown in the chip at its corner. Clicking the chip changes the dialect, the engine, or both, and changing the dialect rewrites the inputs of the document into the new one. Translation between dialects has limits: not every command exists in all four systems. It is a growing capability.

A computer algebra system (CAS) whose dialect is SymPy

A computer algebra environment for the Python scientific stack: SymPy, NumPy, SciPy and Matplotlib.

The commands are SymPy's own, read as mathematics: no imports and no declaring symbols, a free name declares itself, x^2 is a power, 3/2 stays exact, == makes an equation rather than a true/false verdict. Edit a line above and run it again, carry a result forward by its equation label, read output as typeset mathematics, or the same mathematics inline in a text region, and organise the whole with sections, subsections and hyperlinks. In Presentation mode, Export as LaTeX writes the document out as a paper.

SymPy 101, which ships with the ExaktAI Workspace, in two windows: on the left sections two to four, each with what it is on paper and in SymPy, and its exercises open with their solutions folded; on the right, in a window of its own, the example of section thirteen, the vector equation of a plane through three points, computed and plotted in 3-D; both chips read sympy to sympy with the CAS badge lit — The SymPy 101 that ships with the Workspace. On the left, three of its sections, each with its exercises, the solutions folded; on the right, in a window of its own, the example of section 13 run. The chip **(sympy → sympy)** indicates the dialect and the mathematical software that computes. Results are numbered and reusable by their number. The **CAS** badge is lit: `x^2` is a power, `3/2` exact, `==` an equation.

NumPy, SciPy and Matplotlib are bundled beside SymPy and run as themselves: their numbers are machine floats, and a region that computes with them stays a program. The symbolic mathematics is SymPy's; NumPy arrays, SciPy computations and Matplotlib figures keep Python's own semantics.

Help ▸ Tutorials opens eight introductions: SymPy 101, NumPy 101, SciPy 101 and Matplotlib 101; Maple 101, Mathematica 101 and MATLAB 101; and Lean 101. Each one is a Workspace document that runs as you read it, with examples, exercises and their solutions, and any line can be changed and run again. With introductions in several dialects, a new system can be learned next to one you already know.

The Workspace includes an AI assistant beside the document, its own help pages, and a help page for each command it covers in the SymPy, Maple and Mathematica dialects. F1 on a command you typed opens its help page; hovering a typeset function in the output shows how it is written in the dialect, and links to its page. And the Digital Library of Mathematical Functions opens in a window of its own, where an identity on one of its pages is taken into the document, written directly in the document's dialect, ready to use.

Open what you already have

Maple, Mathematica, MATLAB, Jupyter and Python files, decoded natively.

A notebook of your own opens as it was written: its SymPy, NumPy and SciPy code keeps Python's own semantics, and the stack that runs it is included in the Workspace. What is new is around it, the document now being one of your collection, with the mathematical software, the labels and the assistant beside it.

Or the same notebook is imported as a CAS document: the imports and symbol declarations the CAS reading does not need are omitted, the notation becomes the dialect's, and the author's comments become the document's text. Regions that are programs, computing with NumPy or SciPy on machine numbers, stay programs.

The same Jupyter notebook for SymPy open twice in the ExaktAI Workspace: on the left as written, with symbols declared by hand and A**2 in Python notation; on the right imported as a CAS document, where the declarations are gone, the matrices are typeset, and A squared and A times b are shown in CAS notation — One notebook, twice. Opened as written on the left, *imported as a CAS document* on the right, where the declarations the CAS reading does not need are omitted and the notation is read as mathematics: the same computation in its CAS-document form.

The chip at the top right says which reading a document is in: the CAS badge lit for SymPy read as mathematics, dimmed for literal Python. Clicking it rewrites the document's inputs into the other reading, in either direction.

A Maple worksheet (.mw), a Mathematica notebook (.nb), a MATLAB script (.m) or Live Script (.mlx) are read directly, with no Maple, no Mathematica and no MATLAB required on the computer. Where the document's constructs all translate, the bundled SymPy, NumPy and SciPy run the computations written in your imported dialect. For a Mathematica document, you can install the Wolfram Engine, free for non-commercial, personal use, and run it on Wolfram's own computational engine. And if you have Maple, Mathematica or MATLAB, a right click on any line offers to run that line using a different CAS engine.

Two ExaktAI Workspace documents side by side: on the left a MATLAB-notation document whose chip reads matlab to sympy, an ode45 integration and its plot computed by the bundled SymPy, NumPy and SciPy; on the right a Mathematica-notation document, mathematica to sympy, with the right-click menu open on an Integrate line offering Execute in SymPy, Execute in Maple with a check mark and the hint option-as-written, Execute in Mathematica and Execute in MATLAB, and results badged Maple or Mathematica, the software that answered that line. — A MATLAB document and a Mathematica document, both computing on the bundled SymPy, NumPy and SciPy, on a computer with neither installed: the chips read **matlab → sympy** and **mathematica → sympy**. The menu on the right is the other half of that freedom: one line sent to another mathematical software, its answer badged with whichever software computed it.

A MATLAB Live Script opens with its headings, formatted text, lists and figures in place, its code runnable. If you don't have MATLAB installed, the computational software is set to SymPy, the arrays and the differential equations are handled by NumPy and SciPy, and SymPy answers the symbolic commands in the Symbolic Math Toolbox's own spellings: syms, int, solve and taylor among them.

If you already own Maple, Mathematica or MATLAB

Your computational software, your mathematical dialect, and a workspace around them.

Within the ExaktAI Workspace, the Maple dialect on Maple is Maple sent to Maple; the Mathematica dialect on Mathematica is Wolfram Language sent to the Wolfram Engine; the MATLAB dialect on MATLAB is MATLAB sent to MATLAB. The Workspace drives the copy installed on your computer.

Two ExaktAI Workspace documents side by side: on the left a Maple worksheet on Lagrangians in rotating frames, chip reading maple to maple, with vector results carrying equation labels that later lines reference; on the right a Mathematica notebook on classical mechanics, chip reading mathematica to mathematica, ending in a three-dimensional trajectory plotted by Mathematica — **maple → maple** on the left, **mathematica → mathematica** on the right, running with mathematical dialect and software the same, on the copies installed on your computer.

Proofs with Lean

The CAS computes, Lean checks, in the same document.

Lean is chosen from the engine control beside the four CAS, or for one line by right-clicking it: Execute in Lean. A CAS line’s result can also become a Lean theorem to check: right-click, Use as Lean candidate. The goals after each step appear under it, in document order, and a step can be edited in place: the proof is then marked Outdated until Enter checks it again. “Proof checked” appears only for a complete proof with no sorry anywhere it depends on. .lean files open, and a document exports to one. Help > Tutorials > Lean 101 teaches Lean in the Workspace, from a first theorem to induction, ending in a project that explores with a CAS and certifies with Lean.

The theorem odd_leg, its Proof checked verdict, the existential goal, a SymPy solve line giving b = 2k^2 + 2k and c = 2k^2 + 2k + 1, then use with those two sides, the goal it leaves, and ring ending in No goals — Every odd number is a leg of a Pythagorean triple. SymPy, between two proof steps, solves for the other two sides as formulas in k; Lean checks, with `use` and `ring`, that they work for every integer k.

Lean’s symbols, from the Math palette: in a Lean input it shows Lean’s tactics and symbols, and a backslash name such as \forall then a space types the symbol, as in VS Code.

The Math palette in a Lean input, Symbols tab: Logic, Relations and sets, Numbers and arrows; Insert and Operators greyed, being for CAS lines — The first row is the logic Lean’s statements are made of: ∀ for all, ∃ there exists, ¬ not, ∧ and, ∨ or, → implies, ↔ if and only if, ⊤ true, ⊥ false.

Lean in the Workspace →

All your work in progress, kept

Keep a dozen investigations going at once, and have only the ones you need in front of you.

Mathematical work is often several investigations in flight at once: the one you are on, the three you will come back to, the one from last month whose result you now need. The Workspace keeps them as a collection, outputs and context included. Close it and open it again: every document is where you left it, the unsaved ones included, at the line you were editing. Search across the text and the inputs of everything open, filter, bookmark, and put only what you need on the tab bar without discarding the rest.

Two ExaktAI Workspace windows: on the left a Maple document on the retarded and Lienard-Wiechert potentials with the screen split and the workspace panel open, listing five documents as cards with their dialect, whether each is Edited or Saved, and when it was last touched, above a search box and filters by time, CAS and state; on the right the NumPy 101 tutorial — An afternoon's collection, on the left, its document split: the part being read on top, the part being written below, each scrolling on its own. Every open document is a card carrying its dialect, its state and when it was last touched, over a search that reads the text and the inputs of all of them.

Where validated AI mathematics lands

The Workspace is also the reading room for ExaktAI Validation.

When ExaktAI Validation validates an AI's solution, with SymPy, Maple or Mathematica, the result arrives here: an editable document holding the AI's reasoning as narrative and every computation as executable input, already run and already validated. Audit it, change a line, re-run it, extend it. Validated with Maple or Mathematica, the document is in that dialect, and the native .mw or .nb is written beside it.

On the left ExaktAI Validation, an ADMM problem answered by Codex and validated with SymPy in five and a half minutes; on the right the ExaktAI Workspace document that arrived from it, each step of the reasoning a paragraph of text followed by an executable input carrying its own computed result, down to the optimum at minus three and three — Where a validated run lands. ExaktAI Validation checked Codex's ADMM solution step by step with SymPy; the document that arrived from it holds every step as an executable input, so changing a line re-runs the derivation.

What it needs

SymPy, NumPy, SciPy and Matplotlib are bundled and run locally. Maple, Mathematica and MATLAB execution needs those products installed and licensed on your computer. Ordinary document and CAS work is local; no hosted AI is required to use the Workspace.

Translation between dialects covers mathematics, mappings and flow structures, not programs. It grows command by command, and not every command exists in all four systems. Lean is not bundled: Help > How to > Setting up Lean explains how to install it with its Mathlib library, which takes several gigabytes of disk; with Mathlib loaded, a Lean document also takes several gigabytes of memory. An imported document keeps its output without re-executing it, and anything the import cannot decode is kept untranslated. A document exported to another system preserves its contents, but may produce different results when run there.

Acknowledgments

The Workspace stands on open-source work: Python with SymPy, NumPy, SciPy and Matplotlib for the computing; Plotly for the plots; KaTeX and MathJax for the typesetting and MathLive for the formula editor; Tauri for the application itself; Hunspell and its dictionaries for the spelling.

The full third-party notices →

Download

The complete Workspace is free for everybody through June 30, 2027. Licence and availability →

Download

ExaktAI Validation

Its Beta is scheduled for October 15, 2026. Sign up, and we write to you when it opens; a question, or a mathematical problem you would like to see it try, is welcome too.

Your address is used only to write to you about the Beta. Privacy policy →

^* SymPy, NumPy, SciPy and Matplotlib are trademarks of NumFOCUS, Inc., used here to identify the bundled software. ExaktAI is an independent product, not affiliated with, endorsed by, or sponsored by these projects or NumFOCUS. ↩

Maple is a trademark of Waterloo Maple Inc., Mathematica and Wolfram Language of Wolfram Research, Inc., and MATLAB of The MathWorks, Inc., used here to identify the software the Workspace works with. ExaktAI is an independent product, not affiliated with, endorsed by, or sponsored by them.