JuliaLab

A Platform for Julia, Pluto, Mathematica and the Lean Theorem Prover

July 25, 2026 · John Peach

I started using Matlab before grad school which helped because it was the required language for many of the math classes I took, and it was the language of choice at MIT Lincoln Laboratory where I worked after grad school. Matlab is a fairly easy computer language to learn, designed for math and science, and has a well thought out Integrated Development Environment (IDE). The IDE lets you write code in the editor, execute commands and run programs in the Command Window and lets the user click on buttons in the ribbon that run special features of Matlab.

Matlab is great, but it is a commercial product, so you have to pay for a license, currently $150 per year for the core platform. There are toolboxes that extend Matlab’s capabilities, but they add to the base cost. An open-source alternative is GNU Octave which is very similar to Matlab, but not as complete and tends to be quite a bit slower. SciLab, ScicosLab, Euler Math Toolbox and Nelson are all free alternatives, but I thought that the Julia Language might be a better choice.

Julia was developed by Jeff Bezanson and Alan Edelman at MIT and Stefan Karpinski and Viral Shah at UC Santa Barbara beginning in 2009. The syntax is similar to Matlab and it was designed to be a very fast language, but there are no IDEs for Julia that gave the same experience as Matlab until the recent release of Compute42. The most popular IDE for Julia is Visual Studio Code or the open-source equivalent, VSCodium, but they don’t have a Matlab-like ribbon.

Since nothing quite matched what I wanted in a Julia IDE, I decided to build one. As I began working on JuliaLab I realized that including a few related platforms would greatly increase the usefulness of JuliaLab. The platforms that now run in JuliaLab are

• Julia - High performance numerical language for math and science.
• Pluto - A notebook interface for Julia that allows you to write text and equations for interactive documents.
• Wolfram Language - Symbolic calculations and visualizations.
• Lean Theorem Prover - Programming language and proof assistant to guarantee correctness of mathematical proofs.

First, we’ll look at the Integrated Development Environment, giving an overview of each of the tabs and how the ribbon works. JuliaLab is free to download as are all of the component platforms.

The Integrated Development Environment

When you launch JuliaLab you will see the ribbon at the top with tabs for HOME, CODE, FIGURES and VIEW. In the HOME tab there are several groups of related operators. For example, the Directory group will tell you the current directory, allow you to change directories, or show a list of recently accessed directories. The Package Manager helps to add, remove or update Julia packages which are similar to Matlab Toolboxes.

Platforms will start one of the other tools listed above, or let you interact with an Artificial Intelligence assistant. Clicking on any of the buttons in Help opens a separate browser window linked to Julia documentation, examples or the Julia Community where you can ask questions about the language.

On the far left is the Activity Bar with icons for the File Explorer, Search, GitHub Source Control, Run/Debug, Extensions, Testing, Julia, and Wolfram. The panel to the right of the Activity Bar will open an interface for each of the Activity Bar icons. Shown is the File Explorer in my Julia folder. Subfolders may be opened and files may be loaded directly into the Editor by clicking on them.

The CODE tab provides an interface to the code you write. In the center of the window at the top is the Editor, and directly below that is the terminal showing an active Julia REPL (Read-Eval-Print Loop) REPL (Read-Eval-Print Loop): an interactive prompt where you type an expression, the language evaluates it, and the result is printed immediately — the same role MATLAB’s Command Window plays. with the prompt

julia >

Use the REPL to run calculations or generate plots directly in Julia.

The FIGURES tab makes plotting easy. Define variables, e.g. $\theta, y, z$ and then click the Julia icon (three circles) on the Activity Bar. Under Plot Variables, select the variables to plot in the order you want to see them. Clicking $\theta$ first puts it on the $x$-axis, then shift-click $y,z$ for the $y$-axis. Choose the plot type such as Line, Scatter or Bar. Depending on the number and type of variable selected, some options may be grayed-out. Select the style and additional features from AXES, then click the Plot button to generate a plot. You may select New to open a new plot pane, or Reuse to overwrite the existing plot. In this early version of JuliaLab, the Animate group is not working yet.

In Julia you can write variables in the way you’d expect for math,

julia> θ = 0:0.1:2π;

which is not found in many other languages.

The VIEW tab lets you hide or show panes on the main window. You can also toggle the ribbon itself with Ctrl-Alt-H. The Layout Manager is inoperable for this beta version of JuliaLab.

Julia

For anyone who has spent time coding in Matlab, Julia should feel very familiar. There are differences, of course, but the transition shouldn’t be too difficult. The Scientific Modeling Cheatsheet compares syntax across four languages - Matlab, Scilab, Python and Julia. If you want to generate a linearly spaced vector in Julia use A = range(1, 5, length = k) instead of A = linspace(1, 5, k) in Matlab.

This screenshot of the JuliaLab REPL (Command Window in Matlab) looks like this

In Matlab, the vector $b$ would be written as b = [1.0; 2.0] or b = [1.0 2.0]', but Julia simply recognizes it as a 2-element vector.

Pluto

Imagine opening a math or science textbook or reading a technical article where the text and equations are nicely formatted, but you can interact directly with the equations. Change a parameter and the equations and plots change instantly everywhere in the document. This is an example of the Lorenz equations which you can download and run. You can drag the plot around to view it from different angles, too. The color of the line indicates the value of the parameter $t$ which indicates how far along the curve you are. Notice that the plot starts in the outer loops of the right butterfly wing, but quickly switches to the center of the left wing. It spends quite a bit of time ($t = 30 - 40$) in the center of the right side before jumping back.

To write text and equations, you need to learn a little bit about the Markdown language (see How to use Markdown in Pluto). PlutoUI (UI is for User Interface) is the library that lets you include sliders, number fields and other interactive components.

Wolfram (Mathematica)

Mathematica is an interface to the Wolfram Language, a technical computing symbolic and functional programming language built to transform expressions rather than simply calculate numerically. For example, to calculate $\int_0^{\pi} \sin^2 x dx$

Integrate[Sin[x]^2, {x, 0, Pi}]
π/2

returns the precise value of $\pi/2$ instead of the numerical approximation $1.570796$. Mathematica is the notebook front end to the Wolfram Language, much like Pluto is a notebook for Julia. Mathematica is a commercial product of Wolfram Research and is currently priced at $195 per year for a personal license. Wolfram Language is free to download for personal use, and is the computational engine for Mathematica. What makes Wolfram Language useful for JuliaLab is the interface Wolfbook developed by Nikolay Gromov, a professor of theoretical physics at King’s College London.

Follow the Quick Start instructions on the Wolfbook GitHub site to install and activate the Wolfram Engine. JuliaLab is built on VSCode, so you don’t need to install it separately. Wolfbook is intended to be used with the AI agent Copilot, Claude Code or MCP Agents, and I built JuliaLab with an AI assistant that opens an external browser for Claude, ChatGPT or Gemini.

Wolfbook is similar to Pluto in that it is a notebook interface to the Wolfram Language. Here’s a screen grab of the bessel.wb notebook describing Bessel functions:

Wolfbook doesn’t allow you to drag the plot to view it from different angles the way Mathematica notebooks do, so you might consider exporting the data to Julia and plotting there.

Lean Theorem Prover

The Lean Theorem Prover is an open-source, interactive theorem prover and functional programming language originally launched by Leonardo de Moura at Microsoft Research in 2013. Lean is built on a version of the Calculus of Constructions Calculus of Constructions: a formal logical system that unifies proofs and programs — in it, a mathematical proof and a piece of verified code are, structurally, the same kind of object. with inductive types providing a rigorous mathematical framework capable of expressing complex assertions, defining abstract objects, and verifying formal proofs. Lean acts as both a programming language for writing verified software and a metaprogramming environment where you can extend system capabilities and build custom automation directly within the language itself.

To prove mathematical theorems, Lean requires that every assertion and logical step be reduced to foundational axioms and explicit rules of inference. Rather than requiring you to manually write out every granular step, Lean bridges the gap between interactive and automated theorem proving through features like elaboration, type inference, and term rewriting Elaboration: the process by which Lean fills in details you left implicit (like inferred types or omitted arguments) so your shorthand proof becomes a fully explicit one the kernel can check. . Users interactively construct proofs using Lean’s tactic mode or term language within JuliaLab, receiving immediate feedback on goal states and type correctness. When a proof is completed, Lean checks the full proof object to guarantee mathematical soundness, ensuring that complex claims are fully verified down to basic foundational principles.

Lean doesn’t generate the proof for you, but it insists that no critical steps are omitted.

To see how Lean works, let’s start with the classic proof that $\sqrt{2}$ is irrational.

Theorem: $\sqrt{2}$ is an irrational number.

Proof: Suppose that $\sqrt{2}$ is, in fact, rational so that it may be expressed as

for some integers $m$ and $n$, where $m/n$ is in lowest terms. Squaring both sides and rearranging,

so 2 divides $m^2$ meaning that $m$ is even, or $m = 2k$ for some integer $k$. Then

so $n^2 = 2 k^2,$ and thus $n$ is also even. But, this contradicts the assumption that $\gcd(m,n)=1$, so $\sqrt{2}$ must not be rational. $\blacksquare$

The code in Lean:

The proof is on the left and Lean’s InfoView pane is on the right. One thing that feels strange coming from MATLAB is that when this checks, Lean says nothing. No output, no green “PASS”, just a small check mark and an empty message panel. No messages in the InfoView pane means every step held and the proof is complete.

Lean is a programming language which has been extended with a library of formalized mathematics, Mathlib and a similar library for physics, Physlib. There are two recommended resources for doing mathematics in Lean, Theorem Proving in Lean and Mathematics in Lean. For physics, look at Physlib Documentation.

AI Assistance in JuliaLab

Right now, clicking the AI assistant button in the Platforms group doesn’t open an embedded chat panel. Instead, it opens a picker that launches Claude, ChatGPT, or Gemini in your regular web browser. You lose your place in the editor; you’re not getting inline suggestions or a sidebar that sees your code. It’s a convenience shortcut, not an integration.

The long-term goal is a proper AI sidebar inside the workbench, one that can see the file you’re editing, run code in the same REPL you’re using, and (eventually) call into Wolfram or Lean the way Wolfbook already lets Copilot and Claude Code do for Wolfram notebooks. I ran into real obstacles getting there for this release because VSCodium’s serve-web mode has some technical issues around embedded browser panels and Service Worker behavior that I’m still working through.

If you’re trying JuliaLab expecting Cursor- or Windsurf-style inline AI, you won’t find it yet. If you’re fine opening a browser tab to your AI assistant of choice while you work, the current shortcut saves you a few clicks.

JuliaLab Installation

JuliaLab is currently in active MVP (minimum viable product) development — there’s no packaged installer yet, so getting it running means building from source. That’s a five-minute job if you’re comfortable with a terminal, and it means you’re always running the latest code.

What you’ll need first

Two more are detected automatically if present, but aren’t required to launch the app:

• Wolfram Engine (free personal license) — needed only for Wolfbook notebooks
• Lean4, via elan — needed only for Lean4 language support

juliaup and elan are version managers for Julia and Lean respectively — they let you install, switch between, and update language toolchain versions without touching system PATH by hand.

If Julia, Wolfram, or Lean4 aren’t found on first launch, JuliaLab will tell you and point you to the installer, and it will continue to work with just Julia/Pluto.

Windows only, for now. The current build resolves several paths (including the VSCodium binary) as hardcoded Windows paths, so macOS/Linux aren’t supported yet.

Build and run

Open a terminal (PowerShell is fine) and run:

git clone https://github.com/XerxesZorgon/JuliaLab.git
cd JuliaLab
npm install
npm start

npm start does two things in sequence: it compiles the bundled julialab VS Code extension, then launches the Electron shell. The first launch will run dependency detection and create a default workspace folder at ~\JuliaLab.

If you only need to relaunch after a UI-only change (no extension edits), npm run start:fast skips the extension rebuild and starts faster.

A note on what “installed” means right now

This gets you a running development build, not a signed, distributable app, so there’s no Start Menu entry, no auto-update, and no uninstaller. If you’re trying JuliaLab out, please understand that it’s a very early release.

Future Enhancements

Tier 1

• Multivariable plotting: Some capability exists in the FIGURES tab, but it’s incomplete
• Multi-root workspace: Let a Julia working folder and a Lean project be open at once, instead of the workbench (and Julia REPL) switching whenever a Lean project opens.
• Editor run-sections (%% cell execution in .jl files): Matlab’s code-section feature is to divide a script with %% and run one section at a time.
• Auto-load Revise into JuliaLab’s REPL: Changes made to code in the Editor are immediately available in the REPL.

Tier 2

• Workspace / variable browser: A live view of defined variables, their types, sizes, and values, clickable to inspect.
• Debugger integration: Matlab-style breakpoints, step-through, and variable inspection at a breakpoint for Julia.

Tier 3

• Dedicated Wolfram / Lean ribbon tabs: Build commonly used Wolfram and Lean commands into clickable ribbon buttons. Include links to external help sites similar to the Julia sites
• Lean scratchpad: A one-click Mathlib-ready project so Mathlib downloads once, with reserved-name and stable-toolchain guards. Currently, creating a new project that requires Mathlib will make a new folder and install Mathlib in the folder consuming tens of Gb of space.
• First-run onboarding and dependency setup: On first launch, detect missing Julia / Wolfram / Lean and guide the user through setup, instead of silent failures.
• Windows/Mac/Linux packaging and installer.
• Toolchain-drift awareness (Lean Mathlib RC vs. stable default) — a maintenance watch item, already backlogged.
• Build Matlab addpath/genpath equivalents for Julia
• VSCodium front end: I wanted to build JuliaLab using VSCodium, the open-source fork of VSCode, but there was a bug in VSCodium that prevented it from being used. Hopefully the bug will be corrected soon, but if you see any instructions to use VSCodium, just replace it with VSCode for now.

Conclusion

I started this project because I missed something specific: the feeling of opening MATLAB, clicking a button in the ribbon, and having a plot show up with no context-switching, no remembering command syntax, no fighting an editor that wasn’t built for scientists. Julia gave me the speed and the open-source license I wanted, but not that feeling.

What’s here now is an early MVP (minimum viable product) Windows-only, built from source, with a few panels (Animate, Layout Manager) that don’t work yet. But the core works: write Julia in an editor that feels like MATLAB’s, run it in a REPL, plot it from the ribbon, and when the problem calls for it, drop into Pluto for an interactive notebook, Wolfram for exact symbolic answers, or Lean to check that a proof actually holds. That’s not something I’ve found bundled anywhere else, and it’s already how I do my own work.

I still want a real installer, multivariable plotting, a debugger, dedicated Wolfram and Lean ribbon tabs among the many possible features. If you try JuliaLab and hit a wall, or if you build something with it worth sharing, I’d like to hear about it. The code is on GitHub; issues and pull requests are welcome.

Code for this article

• lorenz.jl: A Pluto notebook demonstrating interactivity using the Lorenz attractor as an example.
• bessel.wb: A Wolfram notebook describing the Bessel function.
• sqrt2.lean: Proof the square root of two is irrational using Lean Theorem Prover.
• JuliaLab: Source code for the project.

Software

• Julia - The Julia Project as a whole is about bringing usable, scalable technical computing to a greater audience: allowing scientists and researchers to use computation more rapidly and effectively; letting businesses do harder and more interesting analyses more easily and cheaply.
• Pluto - Pluto is an environment to work with the Julia programming language. Easy to use like Python, fast like C.
• Wolfram Language - Wolfram Language is a symbolic language, deliberately designed with the breadth and unity needed to develop powerful programs quickly. By integrating high-level forms—like Image, GeoPolygon or Molecule—along with advanced superfunctions—such as ImageIdentify or ApplyReaction—Wolfram Language makes it possible to quickly express complex ideas in computational form.
• Lean Theorem Prover - Lean is a functional programming language that makes it easy to write correct and maintainable code. You can also use Lean as an interactive theorem prover.

Image credits

• Sydney Harris: I think you should be more specific here in step two.