Features of the ExaktAI Workspace

Every open document is a tab with its own session, mathematical dialect and computational engine.

Tabs

• A session per document. Each tab has its own session with its settings, text and computations. A new tab starts a fresh session.
• Tabs. A new tab opens beside the current one. The tab bar scrolls horizontally to show more tabs. Tabs also reorder by dragging, close with the x, the middle button or File ▸ Close tab (⌘W). The last five closed tabs can still come back with File ▸ Reopen closed tab (⇧⌘T). A tab shows its dialect in colour, a dot when the document is Edited, a flag when bookmarked, and a pulse while it computes. Hovering shows the file's path and (dialect → engine).
• One tab per file. Opening a file that is already open brings its tab forward.
• The tab menu. A right-click offers Save, Save As, Show in Finder, Bookmark, Draft of this tab, Detach, Close, Close others and Close all.

Windows

• Detach. Window ▸ Detach this tab into its own window moves a document, with its session, into a window of its own. The session continues, with its variables. Closing the window, or its toolbar button Back into the main window, returns the document to the main window. One document is detached at a time.
• Draft. Window ▸ Draft of this tab (⌥⌘D) opens a second window on the same document, for trying things without touching it. The draft can use the variables the document has assigned. Settings choose whether it shares the document's kernel, starts a new one, or asks, and the draft wears a different theme. Window ▸ Promote to the main document (⌥⌘P) sends the selected inputs into the main document, without results. On Maple, Mathematica and MATLAB a draft shares the document's session, so its assignments reach the document.
• Split. View ▸ Split horizontally (⇧⌘\) shows the document twice: a read-only copy above, the editable one below, each scrolling on its own.
• Keep on top. The pin in a title bar keeps that window above the others.
• Presentation and Manuscript. View ▸ Presentation mode (⇧⌘P) hides the toolbar, the tabs and the inputs, and makes the document read-only; Esc leaves it. View ▸ Manuscript mode hides the input prompt and the bookmark flags while the document stays editable. View ▸ Hide computation inputs (⇧⌘D) shows results only.
• Position. The main window reopens where it was, and is brought back inside the screen if the monitor changed.

Several documents compute at once. Each can be stopped, and the time they take can be read.

Running

• Run a line. Enter runs a line and moves to the next, creating one at the end when there is none. Shift+Enter adds a line inside the input. A line ending in a colon runs without displaying its result.
• Run more. In the Evaluate menu, Run selection (⌘↵) runs the selected inputs, Restart and run all (⇧⌘↵) restarts the session and runs everything, and Restart and run to cursor (⌥⌘↵) restarts and runs up to the cursor. The Run all icon takes the three: a click, a Shift-click and an Option-click.
• Restart. Evaluate ▸ Restart session (⇧⌘R) clears the live session and keeps the displayed outputs, so the next run can be compared with them line by line. A restart line inside a document restarts that document's own session.
• Parallel documents. Documents compute at the same time, each on its own session. A run in a background tab leaves the front tab free, and its results land in the tab that ran it. A document is read-only while it computes.
• Warm start. The mathematical software of the document in front starts quietly in the background, so its first line runs without waiting. If none of its lines has run, the software is stopped again when another document comes to the front.
• Stored results. A reopened document shows its stored results, and each line runs when you run it.
• Working folder. Relative file names in a document resolve against the document's own folder.

Stopping

• Stop. The Stop button, or Evaluate ▸ Interrupt (⌘.), stops the document in front. Shift-click on it, or Evaluate ▸ Stop all (⇧⌘.), stops every running document, and a badge on the button counts how many are running.
• What stopping does. A SymPy session keeps its variables and abandons the running line. Stopping a Maple, Mathematica or MATLAB line stops that software; it starts again on the next run, and the status line says that the session's variables are gone.
• Time limit. A Maple, Mathematica or MATLAB line that runs longer than the limit has that software stopped and restarted empty, and the line says so. The limit is 3 minutes, set in Settings; 0 removes it.

Timing

• Stopwatch. Tools ▸ New Stopwatch opens a small window that stays on top. It has no Start button: it starts when any document begins computing and stops when every running document has finished. Each document that finishes adds a lap with its name, so documents computing in parallel list their times in the order they finish.
• Timers. Tools ▸ New Timer takes a name and a duration (45, 45 min, 1h30, 1:30), counts down in a window that stays on top, and chimes at the end. Several timers can run together, and the last ten names are remembered.
• Progress. A line still running shows computing… after a short delay, and its elapsed time from 15 seconds on.
• When a long run ends. A run of more than 10 seconds ends with its elapsed time in the status bar. When the window is not in front, the Dock icon bounces, and a chime is available in Settings.
• Timing report. Tools ▸ Timing report after each run adds a breakdown after every run (kernel, typesetting, layout) and writes it to a log.

The open documents are kept as a collection that survives closing the Workspace.

The collection

• Workspace browser. The ▾ button after the tabs lists every open document as a card with its name, a flag when bookmarked, its software, Edited or Saved, and the date. A click opens it, and Select, then Close, closes several documents at once.
• Search. A search reads titles, paths and every input and text region, with AND, OR, NOT and parentheses, Match case and Whole word.
• Filters. Filters show only the bookmarked documents, those changed within the last days, weeks or months, those computed by a chosen software, or those Edited or Saved. They narrow the tab bar as well, a banner offers to clear them, and they persist.

Saving

• Save. Save writes to a new file and then replaces the old one, so a crash cannot leave it empty. File ▸ Save As (⇧⌘S) offers ExaktAI (.eai) and Lean (.lean) in the save panel on macOS, and in two short dialogs on Windows and Linux.
• Maple, Mathematica and MATLAB saving. Workspace Plus from July 1, 2027 File ▸ Save As also offers Maple (.mw), Mathematica (.nb) and MATLAB Live Script (.mlx). A save in another format is an export, and the document stays as it was.
• Edited. The title bar and the tab say Edited when the document differs from its last saved state, and undoing back to it clears the mark.
• Two baselines. Evaluate ▸ Restore original (⌥⌘R) returns the document to what it started from: the file as opened, the import as reconstructed, or a blank input. Evaluate ▸ Revert to Saved (⇧⌥⌘R) returns it to the last saved file. Both restart the session and are one undo step.
• Undo. Each tab keeps 100 steps of undo and redo.

Recovery

• Sessions. Settings ▸ Session chooses Work in progress, Editor or Classic. Work in progress never asks on closing and reopens every tab as it was, unsaved documents included. Editor reopens the saved files and asks Save All, Don't Save or Cancel. Classic starts a blank document.
• Continuous backup. The whole workspace is saved as you work. After a crash or a forced quit, the last state returns, with stored outputs shown and nothing executed.

Opening files

• Open. File ▸ Open (⌘O) takes several files at once, File ▸ Open Recent keeps the last ten, a file dropped on the window opens as a tab, and a double-click or Open With in the operating system opens it in the Workspace. The Workspace registers .eai and .sympy as its own, and is offered for .ipynb, .nb, .mw, .py, .m and .mlx.
• Updates. A gold arrow in the title bar lights when a newer build exists. One click downloads and installs it, and the Workspace relaunches only when asked. Help ▸ Check for updates checks at once and says the result in the status bar.

A document is written in a dialect and computed by mathematical software. The two are chosen separately.

Mathematical software

• SymPy stack. SymPy 1.14, NumPy, SciPy and Matplotlib on Python 3.13 are bundled and run on every supported machine, with nothing to install.
• Maple. Workspace Plus from July 1, 2027 Maple runs from your own installation, in a persistent session of its own per document. The newest installed Maple is found automatically, and Maple 2026 and 2025 are the tested versions.
• Mathematica. Workspace Plus from July 1, 2027 Mathematica runs as a persistent kernel per document, with no front end needed, and so does the Wolfram Engine, free for non-commercial, personal use. Mathematica's licence allows two kernels at once, and a third document gets a message saying so. A Settings option lets documents take turns on the two seats, and a document whose kernel is taken is rebuilt by re-running its earlier lines when it returns.
• MATLAB. Workspace Plus from July 1, 2027 MATLAB runs from your own installation in a persistent session, started in the background. Figures it draws appear under the lines that made them.
• Lean. Lean is a fifth computational engine, for proofs; a Lean document is written in Lean and checked by Lean. Proofs with Lean describes it below.
• Separate processes. Each document's mathematical software runs as a process of its own. If that process ends unexpectedly, the line that was running says so, and the next run starts a new one.

Choosing

• The chip. A chip in the title bar, at the top right, reads (dialect → engine), the engine being the mathematical software. Clicking either side opens its chooser, and a double-click on a name sets both. The four dialects and four mathematical software systems give sixteen pairings.
• Software that is missing. Mathematical software that is not installed is greyed out in the engine chooser. Its dialect is never greyed, so a Maple worksheet can be read and run on SymPy in the Maple dialect.
• Defaults. Settings ▸ Input dialect and Engine set the defaults for new documents.
• CAS notation. In the SymPy dialect a CAS badge on the chip switches CAS notation on or off, rewriting every input in one undo step. Under CAS notation ^ is a power, 3/2 stays exact, == forms an equation, |x|, x! and f'(x) read as mathematics, and a free name declares itself.
• Evalb and Identical. Evalb decides a relation, and Identical compares expressions strictly. === and =!= test equality of values, and $ and seq build sequences.

Translation

• Changing the dialect. Changing a document's dialect shows every input in the new dialect at once, without running anything. Each line keeps the text it was written in, so going to another dialect and back restores it exactly.
• Changing the engine. Changing the engine leaves the outputs and their badges as they are. Later runs translate each line from the dialect it was written in to the new software, which starts with an empty session.
• Tables. Maple and Mathematica translate directly into each other, MATLAB translates directly into both, and each dialect translates to and from SymPy. Maple and Mathematica to MATLAB go through SymPy.
• Flow structures. if, for, while, procedures and functions, try and catch, return, break and next translate between the four dialects.
• What cannot be translated. When a command has no equivalent in the target, a message says so before anything is computed, and names the closest command when there is one. A line that cannot be translated is shown as written, with a note under it. When the closest command was used, the result says which.
• TranslateTo. TranslateTo(expression, dialect) translates one expression and says what it could not translate.
• Limits. Translation covers mathematics, mappings and flow structures, and grows command by command; not every command exists in all four systems. Physics, tensors and units have no tables between dialects.

Execute in another CAS

• One line on SymPy. A right-click on an input offers Execute in SymPy. The line is translated, computed on SymPy, and its answer comes back with a SymPy badge. The document's own software and dialect stay as they are.
• One line on a commercial engine. Workspace Plus from July 1, 2027 The same menu offers Execute in Maple, Mathematica or MATLAB. The line is translated, computed in that software, and its answer comes back with a badge naming it.
• As written. An Option-click sends the line untranslated, for what the document's dialect cannot express.
• Sticky. A plain re-run of that line goes to the same software, and Run all honours each line's choice.

Python and other languages

• Python regions. A Python region runs as Python, in the same session as the CAS regions beside it. Matplotlib figures appear inline.
• Your own SymPy. Settings ▸ Use my own SymPy uses a newer SymPy from a folder you choose, from the next start, after checking that it loads and computes; NumPy, SciPy and Matplotlib stay the ones included.
• More packages. Further Python packages install into a per-user folder with one pip line, and stay across updates. pandas, torch and jax are not bundled.
• MATLAB dialect without MATLAB. MATLAB source runs on SymPy, NumPy, SciPy and Matplotlib: matrices, ode45, plot and its relatives, and the Symbolic Math Toolbox's own spellings (syms, int, solve, taylor, fourier). A documented subset is covered. With MATLAB installed, a line MATLAB cannot answer is retried on SymPy and wears the SymPy badge.
• MATLAB to Maple. A MATLAB line sent to Maple goes first through Maple's own translator.

Setup

• Check CAS and AIs. Tools ▸ Check CAS and AIs lists Maple, Mathematica, MATLAB, Lean and the AIs, with where each was found. Each installation found is started once and asked 1 + 1, so one that does not start shows its own error before a document meets it.
• Locating an install. For software that is not found, the panel says what to type in that program to learn its folder, and accepts a pasted path or a folder chosen with Locate. The location is remembered.

Input is typeset as you write it, and stored as plain text.

Input

• Typeset input. An input line is drawn as mathematics: identifiers in italic, standard functions upright, and :=, ->, >=, <=, != drawn as ≔, →, ≥, ≤, ≠. What is stored is the plain one-line text, and copying always gives that text.
• Fractions, powers, subscripts. Typing / draws a stacked fraction with the cursor in the denominator, ^ opens an exponent, and a double underscore opens a subscript (not in Mathematica documents). The right arrow moves out of the fraction, exponent or subscript. Roots and the other templates come from the Math palette, and Settings can turn the 2-D entry off.
• Spacing. Binary operators get their spaces as they are typed. Settings can show a blank between operands as a dot, for multiplication.
• Completion. A list opens after three characters and narrows as you type: your own names first, then the dialect's commands. Enter or Tab accepts, and ⌃Space opens it at once.
• Help at the cursor. F1 on a command opens its help page in the document's dialect, and an input that is just ?name does the same; Help ▸ Command help opens the help window.

Palettes

• Math palette. View ▸ Math palette (⇧⌘M) opens the palette: Insert, Operators, Greek, Tactics and Symbols, with each construct spelled for the dialect of the line you are in. One search field takes a name, a symbol or a backslash abbreviation such as \alpha. It docks in the header or floats.
• Format palette. Format ▸ Format palette (⌘T) opens the palette: bold, italic, underline, strikethrough, alignment, lists, font and colour. On a computation input the formatting applies to the whole line.

Text, links and pictures

• Text regions. Prose is rich text with bold, italic and underline (⌘B, ⌘I, ⌘U, or the Format menu), lists, and tab stops of 2, 4 or 8. Selecting 1-D mathematics in prose and pressing F5, or Edit ▸ Display as math, typesets it inline; with nothing selected, F5 opens a small entry box.
• Equation references. Insert ▸ Equation label (⌘L) followed by a number inserts a live reference to that result, in an input or in prose.
• Markers, bookmarks and links. Insert ▸ Marker (⌥⌘M) flags a region, and View ▸ Next marker (⌥⌘↓) and Previous marker (⌥⌘↑) walk them. Insert ▸ Bookmark (⌥⌘B) names one, and View ▸ Go to bookmark (⇧⌘B) lists them. Insert ▸ Hyperlink (⌥⌘K) turns the selected words into a link to a bookmark, and a link whose bookmark is gone is marked.
• Images. Insert ▸ Image embeds a PNG, JPEG, GIF or WebP in the document, resizable by its corner. A picture dropped on the window is inserted the same way.
• Links out. A web link in prose opens in the browser.

Structure

• Sections. Headings have six levels and fold. In the Insert menu, Move region in (new section) (⌘]) moves a region into a new section, Move region in (⇧⌘]) moves it in, and Move region out (⌘[) moves it out. View ▸ Sections ▸ Expand All (⌥⌘]) and Collapse All (⌥⌘[) work on every heading at once.
• Regions. The Insert menu places a computation region below (⌘J) or above (⌘K), or a text region below (⇧⌘J) or above (⇧⌘K). Edit ▸ Convert region (F6) turns a text region into a computation and back, and Edit ▸ Delete region (⌘⌫) deletes a region with its result.
• Selection. A selection runs across regions by dragging, Shift-click or Shift+arrows, and Edit ▸ Select All (⌘A) takes the whole document. Cutting, copying and pasting regions keeps their dialect and outputs.
• Find and replace. Edit ▸ Find (⌘F) searches inputs, prose, headings and plain-text results, with Whole word and Match case; matches inside folded sections are revealed. Edit ▸ Find and Replace (⌥⌘F) replaces one match or all, as one undo step. Results are never rewritten.

Look

• Themes. ExaktAI, Dark and Light. Plots and line art follow the theme.
• Zoom. View ▸ Zoom ▸ Zoom In (⌘=) and Zoom Out (⌘-) scale the document from 60% to 260%, and Actual Size (⌘0) returns to 100%.
• Toolbar. The toolbar shows icons, or icons with text, and can hide until the title bar is clicked.
• Spelling. Spell checking in English, French, Spanish and Brazilian Portuguese covers prose only, and is off until switched on in Settings. Tools ▸ Check spelling in the document marks the whole document once.
• Shortcuts. Help ▸ Keyboard shortcuts lists every key, grouped by menu, with a filter.

Results are typeset, numbered and reusable, whichever software computed them.

Results

• Typeset results. Results are drawn as mathematics in the document's notation, with long equations wrapped to the window. A result from other software is typeset in the dialect's notation when it translates back, and keeps that software's own display, under its badge, when it does not.
• Text and messages. Errors and printed text are selectable and keep their line breaks. A message a command prints, such as a Maple userinfo, a Mathematica message or a Physics banner, appears as a muted line above the result.
• Errors. An error is written for the reader in one clause, such as an unknown name or a matrix that is not invertible.
• Hover. Hovering a function in a result shows its name in the document's dialect, and a click on the tip opens its help page.
• Animations. A Mathematica Animate, ListAnimate or Manipulate of one variable plays in the document, with a play button and a slider; a saved document plays the frames it stored.
• Large values. A Mathematica value too large to typeset is shown shortened with a notice, and stored whole, so a later reference still uses the whole value.
• Copy. A right-click on a result offers Copy, in the document's dialect, and Copy as LaTeX.

Labels and references

• Equation labels. Every result carries its number at the right. ((n)) refers to result n and stays live: it survives re-runs, can be used in a line computed by other software, and is translated when used. A reference that cannot resolve says why, and is drawn dimmed.
• Last results. %, %% and %%% are the last three results in the order they ran (ans in MATLAB).
• Go to. View ▸ Go to (n) (⇧⌘G) jumps to a result by its number.
• Removing results. View ▸ Remove all results from display (⌘D) hides them while their labels and references still resolve. Edit ▸ Clear all results deletes results, values and labels.

Mathematics

• Exact and approximate. 3/2 stays exact, and a decimal of more than 17 digits keeps all of them. N(x, 30) gives 30 digits and translates to evalf[30], N[x, 30] and vpa. Precision is that of the software computing.
• Assumptions. In the SymPy dialect, Assume, assuming, Is, Coulditbe and additionally follow Maple's models, persistent or for one line. Every free name starts as a plain symbol, and relations stay inert until Evalb decides them.
• Physics and tensors. With Maple computing, Physics, tensors and Setup run in your Maple, with their outputs typeset, including imported ones.
• Units. Units follow the software in use: Unit in Maple, Quantity in Mathematica, sympy.physics.units in SymPy and symunit in MATLAB.

Plots

• Interactive plots. Plots are drawn with Plotly. Hovering reads exact values, dragging a rectangle zooms, a double-click autoscales, axes pan, and a click on the legend hides a curve. A 3-D plot rotates with the drag and zooms with the wheel, and Reset camera returns it.
• Following the theme. Plots take the theme's ink and re-tint when the theme changes. Paper output is black on white.
• SymPy plotting. plot, plot3d, plot_parametric, plot_implicit, plot_contour and complexplot3d draw with Plotly. complexplot3d plots the height |f| coloured by the argument of f. Poles leave gaps, and a plot whose function is undefined over the whole range says so.
• Maple plots. With Maple computing, a plot line runs in Maple and its plot structure is read into an interactive plot: curves, legends, colours, labels, view, shading and camera. A density plot Maple draws as an image is shown as an image.
• Mathematica and MATLAB. Mathematica's 2-D curves, surfaces and contours are interactive, and graphics with shapes, text or filled regions appear as the software's own picture. MATLAB figures appear as images under the lines that made them.
• Matplotlib. A Matplotlib figure appears inline as a still picture.
• Engine plots. Settings ▸ Engine plots chooses interactive plots or the software's own picture. A right-click on an imported plot offers Import plot as an image.
• Stored plots. A plot reopens interactive without running again, and the plots stored in Maple worksheets open as interactive plots.

Files from other systems open as documents, and documents export to other systems.

Opening

• Formats. The Workspace opens its own .eai, and Maple worksheets (.mw), Mathematica notebooks (.nb), Jupyter notebooks (.ipynb), Python scripts (.py), MATLAB scripts (.m) and Live Scripts (.mlx), Lean files (.lean) and Markdown (.md). None needs the originating system installed. An opened foreign file is a new document, and the original file is never overwritten.
• Maple worksheets. A worksheet's sections and headings, prose, typeset input, stored outputs, equation labels, bookmarks and links, lists and tables, stored plots and drawings open as they were, and the stored outputs are kept without running them.
• Mathematica notebooks. Title, section and text cells, input and output cells, and display formulas open, with stored output decoded from its boxes. A graphic is dropped from the output, and the input line draws it again when run.
• Jupyter and Python. A notebook opens as it was written, with its saved outputs, and is never run on opening. A script's docstring and comments become prose. Python keeps Python's meaning, and a notebook opens with CAS notation off so Run all reproduces it.
• MATLAB. Scripts and Live Scripts open as MATLAB documents with no MATLAB installed. A Live Script keeps its headings, formatted text, links, equations, lists and figures.
• Markdown. A Markdown file opens as text regions, with its math typeset, which makes it the way to open an AI chat saved as Markdown.
• Import as a CAS document. File ▸ Import as a CAS document converts a notebook or script into the dialect's notation: the declarations and imports the CAS reading does not need are left out, print(x) becomes x, and comments become prose. Regions that call NumPy, SciPy or Matplotlib stay Python. The status line says what was removed.
• Switching readings. The CAS badge converts a document between Python as written and CAS notation, in either direction, in one undo step.

Exporting

• Export As. File ▸ Export As writes LaTeX, Lean source or PDF.
• Maple, Mathematica and MATLAB export. Workspace Plus from July 1, 2027 File ▸ Export As also writes a Maple worksheet, a Mathematica notebook or a MATLAB Live Script. An export is a transcription for the other system: inputs are translated and not re-run, so results there may differ.
• Worksheets and notebooks. A .mw export carries the headings, text, inputs and results, and a .nb export carries In and Out cells with the labels. References to results are replaced by their values or by Out[k].
• LaTeX. A LaTeX export is an article: the first prose block is the title, headings are sections, labelled results are numbered equations, long equations are broken, and bookmarks are labels and references.
• A paper from Presentation mode. A document exported while presenting, or with its inputs hidden, has results and text only.
• Print and PDF. File ▸ Print (⌘P) prints on white paper and offers Save as PDF. Export As ▸ PDF keeps the theme.
• Lean source. A .lean export writes each Lean input once, with CAS lines and prose as comments, and first checks again the inputs that had passed.
• Limits. Plots and pictures are not carried into .mw, .nb or LaTeX exports. There is no export to .ipynb or .py. A Live Script's saved outputs are not reconstructed, and Maple Sketch and OLE objects are left out.

The help pages, tutorials and how-to documents are part of the Workspace and open without a network.

Command help

• Command help. Help ▸ Command help opens a window with the page for a command in the active document's dialect: Maple, Mathematica, MATLAB, SymPy or Lean. It has a search that shows a page as you type, Back and Forward, and a category browser.
• Pages. Maple, Mathematica and MATLAB have more than a hundred authored pages each, Lean has 61, and SymPy's come live from its own documentation. A page has the calling sequence, a description, examples in the document's dialect, related commands and, when the vendor has one, a link to the official page.
• Examples. Clicking Examples copies a page's examples, with their results, and pasting them into a document gives a heading, text and runnable inputs.
• Lean names. A Lean or Mathlib name without an authored page is answered by the Lean installed on your computer.
• FunctionWizard. FunctionWizard(f) builds a dossier of a function, one folded heading per topic, then a plot and a link to its DLMF page.
• DLMF. Tools ▸ DLMF opens NIST's Digital Library of Mathematical Functions in a window. A formula from a page lands in the document, in the document's dialect.

Learning

• Tutorials. Help ▸ Tutorials has SymPy 101, Maple 101, Mathematica 101, MATLAB 101, NumPy 101, SciPy 101, Matplotlib 101 and Lean 101. They are live documents: their results are stored, and every input runs on your own software.
• SymPy in the Workspace. Help ▸ SymPy in the Workspace has SymPy as a CAS, Evalb and Identical, and a page on bringing your own Python and SymPy code.
• How to. Help ▸ How to holds Setting up an AI, How the AI Assistant works, Setting up Lean and Uninstalling.
• The Workspace help. Help ▸ ExaktAI Workspace help (⇧⌘/) is a document of its own, opened once after each update.
• Reporting. Help ▸ Report a problem opens the report form with the version, the system and the document's mathematical software filled in. A failure from the kernel log can be included, shown on the form first. Questions and ideas opens its form too.

An assistant window beside the document, answering through the AI you choose.

Using it

• The assistant. Tools ▸ AI Assistant opens a window beside the document. Answers appear with their mathematics typeset.
• Seven AIs. Claude, ChatGPT, Gemini, Groq, DeepSeek, Grok and Mistral are offered. Claude and ChatGPT are reached through their command-line programs and your own sign-in, Gemini through its program or a free key, and Groq, DeepSeek, Grok and Mistral through an API key. Gemini and Groq have free keys. An AI is offered when it is reachable on your computer, and Tools ▸ Check CAS and AIs says what is missing for the others.
• Keys. A key you enter is kept in the macOS login Keychain, or in a private file in your home folder on Windows and Linux, and is sent only to its provider.
• One conversation, several AIs. You can change AI in the middle of a conversation, and each AI is given what it has not yet seen, labelled with who said it.
• History. Past conversations are listed at the left, newest first, with a filter. The last 200 are kept on your computer, and any can be continued.
• Stop. A square in the input box, or Esc, stops the request.

In the document

• Place in the document. An icon under an answer places it below the cursor: prose as text regions, headings as headings, formulas as typeset inline math, and code as runnable inputs that have not been run. It is one undo step.
• Formulate. ⌘↵ in the assistant asks the AI to write your request as input in the document's dialect. It arrives as inputs that have not been run, one per line, with ((n)) references kept, and Enter runs them.
• Units. The AI is asked to spell units in each dialect's own way.
• Saved chats. An AI chat saved as Markdown opens as a document.

What is sent

• Data. A question, the earlier turns of the conversation and a short formatting instruction go from your computer straight to the AI you chose. The document stays on your computer, except for what you write in the question. Conversations are kept as files on your computer.

Lean checks the proofs, in the same document as the computations.

Checking

• Lean as a computational engine. Lean is chosen from the engine control, or for one line with a right-click, Execute in Lean. It runs on your own Lean, and on Mathlib when you have it.
• Enter checks. Enter checks the Lean inputs in order. The first check runs on core Lean at once while Mathlib loads, and a result that needs Mathlib is rechecked with it.
• Goals under each step. Each tactic becomes a step showing the goals left after it, with case names, typeset as mathematics where Lean's terms allow it. A long proof folds to its header and its failing steps.
• Verdicts. Proof checked appears for a complete proof with no sorry anywhere it depends on. The other verdicts are Proof incomplete, Check failed, Blocked by an earlier error, Not checked, Evaluated and Definition accepted, and an axiom outside Lean's standard three is named.
• Editing. A step can be edited in place; the proof is marked Outdated until Enter checks it again. At rest a statement is typeset, and a click opens its source.
• Saved check. A reopened document shows Saved check until Enter checks it again on this computer.

With the CAS

• A computation between two steps. Insert CAS computation here, on a step's right-click menu, places a CAS line between two proof steps.
• Use as Lean candidate. A right-click on a CAS line with a result asks the Workspace to write the theorem the result claims, with the hypotheses it needs. Lean checks it.
• Check all. Check all Lean inputs runs every one in order and stops at the first failure.
• Try this. When Lean suggests a replacement, an Apply button under its message makes the edit and checks again.

Around Lean

• Palette and typing. The Math palette has Lean's tactics and symbols, and a backslash name such as \forall followed by a space types the symbol.
• Files. .lean files open as one Lean input, and a document exports to one.
• Help and teaching. Lean has its own command help, Lean 101 teaches it, and Setting up Lean describes the installation.
• What it needs. Lean is not bundled. With Mathlib it takes several gigabytes of disk, and a Lean document with Mathlib loaded takes several gigabytes of memory.

Lean in the Workspace →   Lean 101 →

Where choices are kept, which machines are supported, and what stays on yours.

Settings

• Settings. Settings (⌘,), in the ExaktAI Workspace menu on macOS, opens with a search field. It holds the default dialect and engine, the theme, the toolbar, the session mode, the filters, drafts, the finish notice and its chime, figures, spelling and its language, tab width, engine plots, CAS notation, engine warm-up, Mathematica seat sharing, the time limit, dot multiplication and 2-D input. On Windows it is Tools ▸ Options, and on Linux Edit ▸ Preferences.

Platforms

• Supported machines. macOS on Apple Silicon and Intel, Windows on x86 and arm, and Linux on x86 and arm (Debian and Ubuntu). Windows and Linux show Ctrl and Alt where macOS shows ⌘ and ⌥.
• Software by machine. Maple has no Linux arm build, and on Windows arm it runs under emulation. MATLAB R2026a has no Intel Mac build. The tested versions are on the download page.
• Uninstall. Help ▸ Uninstall removes the Workspace and its settings, and keeps your documents, assistant conversations and keys.

On your computer

• Local computing. Documents, results, the SymPy stack and your own Maple, Mathematica and MATLAB run on your computer. No hosted AI is needed to use the Workspace.
• Language. The Workspace's menus are in English. Spell checking covers four languages, and AIs answer in the language of the question.