Jupyter Notebook

Kleis provides Jupyter kernel support, allowing you to write and execute Kleis code in Jupyter notebooks. This is ideal for:

JupyterLab launcher with Kleis and Kleis Numeric kernels

• Interactive exploration of mathematical concepts
• Teaching mathematical foundations
• Documenting proofs and derivations
• Numerical computation with LAPACK operations
• Publication-quality plotting with Lilaq/Typst integration

Quick Start

cd kleis-notebook
./start-jupyter.sh

This will:

1. Create a Python virtual environment (if needed)
2. Install JupyterLab and the Kleis kernel
3. Launch JupyterLab in your browser

Installation

Prerequisites

1. Python 3.8+ with pip
2. Kleis binary compiled with numerical features:

cd /path/to/kleis
export Z3_SYS_Z3_HEADER=/opt/homebrew/opt/z3/include/z3.h  # macOS Apple Silicon
cargo install --path . --features numerical

Note: The --features numerical flag enables LAPACK operations for eigenvalues, SVD, matrix inversion, and more.

Install the Kernel

cd kleis-notebook

# Option 1: Use the launcher script (recommended)
./start-jupyter.sh install

# Option 2: Manual installation
python3 -m venv venv
source venv/bin/activate
pip install -e .
pip install jupyterlab
python -m kleis_kernel.install
python -m kleis_kernel.install_numeric

Using Kleis in Jupyter

Creating a Notebook

1. Start JupyterLab: ./start-jupyter.sh
2. Click New Notebook
3. Select Kleis or Kleis Numeric kernel

Example: Defining a Group

structure Group(G) {
    operation (*) : G × G → G
    element e : G
    
    axiom left_identity: ∀(a : G). e * a = a
    axiom right_identity: ∀(a : G). a * e = a
    axiom associativity: ∀(a b c : G). (a * b) * c = a * (b * c)
}

Example: Testing Properties

example "group identity" {
    assert(e * e = e)
}

Output:

✅ group identity passed

Example: Numerical Computation

eigenvalues([[1.0, 2.0], [3.0, 4.0]])

Output:

[-0.3722813232690143, 5.372281323269014]

REPL Commands

Use REPL commands directly in notebook cells:

Jupyter Magic Commands

Numerical Operations

When Kleis is compiled with --features numerical, these LAPACK-powered operations are available:

Eigenvalue Decomposition

// Compute eigenvalues
eigenvalues([[4.0, 2.0], [1.0, 3.0]])
// → [5.0, 2.0]

// Full decomposition (eigenvalues + eigenvectors)
eig([[4.0, 2.0], [1.0, 3.0]])
// → [[5.0, 2.0], [[0.894, 0.707], [-0.447, 0.707]]]

Matrix Factorizations

// Singular Value Decomposition
svd([[1.0, 2.0], [3.0, 4.0], [5.0, 6.0]])
// → (U, S, Vt)

// QR Decomposition
qr([[1.0, 2.0], [3.0, 4.0]])
// → (Q, R)

// Cholesky Decomposition (symmetric positive definite)
cholesky([[4.0, 2.0], [2.0, 5.0]])
// → Lower triangular L where A = L * L^T

// Schur Decomposition
schur([[1.0, 2.0], [3.0, 4.0]])
// → (U, T, eigenvalues)

Linear Algebra

// Matrix inverse
inv([[1.0, 2.0], [3.0, 4.0]])
// → Matrix(2, 2, [-2, 1, 1.5, -0.5])

// Determinant
det([[1.0, 2.0], [3.0, 4.0]])
// → -2

// Solve linear system Ax = b
solve([[3.0, 1.0], [1.0, 2.0]], [9.0, 8.0])
// → [2.0, 3.0]

// Matrix rank
rank([[1.0, 2.0, 3.0], [4.0, 5.0, 6.0], [7.0, 8.0, 9.0]])
// → 2

// Condition number
cond([[1.0, 2.0], [3.0, 4.0]])
// → 14.933...

// Matrix norms
norm([[1.0, 2.0], [3.0, 4.0]])
// → Frobenius norm

Matrix Exponential

// e^A (useful for differential equations)
expm([[0.0, 1.0], [-1.0, 0.0]])
// → rotation matrix

Built-in Functions Reference

Important: These functions perform concrete numeric computation. They cannot be used in symbolic contexts such as structure definitions, axiom declarations, or abstract proofs. They are designed for interactive exploration, plotting, and numerical analysis.

Math Functions

Sequence Generation

Random Number Generation

These use a deterministic pseudo-random number generator (LCG) for reproducibility.

Vector Operations

List Manipulation

Pair Operations

Why Numeric-Only?

These functions are implemented in Rust for performance and produce concrete values:

// ✅ Works: Concrete computation
let xs = linspace(0, 6.28, 10)
let ys = list_map(λ x . sin(x), xs)
diagram(plot(xs, ys))

// ❌ Does NOT work: Cannot use in axioms
structure MyStructure(T) {
    axiom bad: sin(x) = cos(x - pi()/2)  // ERROR: sin/cos/pi are numeric
}

For symbolic mathematics, define your own abstract operations:

// ✅ Correct: Define sin symbolically
structure Trigonometry(T) {
    operation sin : T → T
    operation cos : T → T
    constant π : T
    
    axiom shift: ∀(x : T). sin(x) = cos(x - π/2)
}

Matrix Syntax

Matrices can be specified using nested list syntax:

// 2×2 matrix (row-major order)
[[1, 2], [3, 4]]

// 3×3 identity matrix concept
[[1, 0, 0], [0, 1, 0], [0, 0, 1]]

// Column vector as 3×1 matrix
[[1], [2], [3]]

// Row vector as 1×3 matrix
[[1, 2, 3]]

Session Persistence

Definitions persist across cells within a session:

Cell 1:

define square(x) = x * x

Cell 2:

example "use square" {
    assert(square(3) = 9)
}

Output:

✅ use square passed

Use %reset to clear all definitions and start fresh.

Tips for Effective Notebooks

1. Start with imports and definitions at the top
2. Use example blocks for testable assertions
3. Use :eval for quick numerical calculations
4. Use :verify for Z3-backed proofs
5. Document with markdown cells between code
6. Save frequently - Kleis notebooks are standard .ipynb files

Troubleshooting

“kleis binary not found”

Install Kleis with:

cd /path/to/kleis
export Z3_SYS_Z3_HEADER=/opt/homebrew/opt/z3/include/z3.h
cargo install --path . --features numerical

Numerical operations return symbolic expressions

Make sure Kleis was compiled with --features numerical:

cargo install --path . --features numerical

Kernel dies unexpectedly

Check the terminal for error messages. Common causes:

• Z3 timeout on complex verification
• Memory issues with large matrices

Imports fail (stdlib not found)

When running Jupyter from a directory other than the Kleis project root, stdlib imports may fail:

Error: Cannot find file: stdlib/prelude.kleis

Solution: Set the KLEIS_ROOT environment variable to point to your Kleis installation:

export KLEIS_ROOT=/path/to/kleis
jupyter lab

Or add it to your shell profile (~/.bashrc, ~/.zshrc):

export KLEIS_ROOT="$HOME/git/cee/kleis"

The Kleis kernel automatically searches for stdlib in:

1. $KLEIS_ROOT/stdlib/ (if KLEIS_ROOT is set)
2. Current working directory
3. Parent directories (up to 10 levels)

Unicode input

Use standard Kleis Unicode shortcuts:

• \forall → ∀
• \exists → ∃
• \in → ∈
• \R → ℝ
• \N → ℕ
• \Z → ℤ

Example Notebook

Here’s a complete example exploring matrix properties:

Cell 1: Setup

// Define a 2×2 matrix
let A = [[1.0, 2.0], [3.0, 4.0]]

Cell 2: Basic properties

det(A)        // → -2
trace(A)      // → 5 (not yet implemented, use 1+4)

Cell 3: Eigenvalues

eigenvalues(A)
// → [-0.372..., 5.372...]

Cell 4: Verify Cayley-Hamilton

// A matrix satisfies its characteristic polynomial
// For 2×2: A² - trace(A)*A + det(A)*I = 0
// This is verified numerically by the eigenvalue product

Cell 5: Matrix inverse

let Ainv = inv(A)
// Verify: A * Ainv should be identity
// (Matrix multiplication coming soon!)

Plotting

Kleis integrates with Lilaq (Typst’s plotting library) to generate publication-quality plots directly in Jupyter notebooks. The API mirrors Lilaq’s compositional design, making it easy to create complex visualizations.

Requirements

• Typst CLI must be installed: brew install typst (macOS) or see typst.app
• Lilaq 0.5.0+ is automatically imported

Compositional API

Kleis uses a compositional plotting API where:

• Individual functions (plot, scatter, bar, etc.) create PlotElement objects
• The diagram() function combines elements and renders to SVG
• Named arguments (key = value) configure options

diagram(
    plot(xs, ys, color = "blue"),
    scatter(xs, ys, mark = "s"),
    bar(xs, heights, label = "Data"),
    title = "My Chart",
    xlabel = "X-axis",
    theme = "moon"
)

Plot Functions

Data Generation Functions

Example: Grouped Bar Chart with Error Bars

let xs = [0, 1, 2, 3]
let ys1 = [1.35, 3, 2.1, 4]
let ys2 = [1.4, 3.3, 1.9, 4.2]
let yerr1 = [0.2, 0.3, 0.5, 0.4]
let yerr2 = [0.3, 0.3, 0.4, 0.7]

let xs_left = list_map(λ x . x - 0.2, xs)
let xs_right = list_map(λ x . x + 0.2, xs)

diagram(
    bar(xs, ys1, offset = -0.2, width = 0.4, label = "Left"),
    bar(xs, ys2, offset = 0.2, width = 0.4, label = "Right"),
    plot(xs_left, ys1, yerr = yerr1, color = "black", stroke = "none"),
    plot(xs_right, ys2, yerr = yerr2, color = "black", stroke = "none"),
    width = 5,
    legend_position = "left + top"
)

Example: Bar Chart with Dynamic Annotations

let xs = [0, 1, 2, 3, 4, 5, 6, 7, 8]
let ys = [12, 51, 23, 36, 38, 15, 10, 22, 86]

// Dynamic annotations using list_map and conditionals
let annotations = list_map(λ p . 
    let x = fst(p) in
    let y = snd(p) in
    let align = if y > 12 then "top" else "bottom" in
    place(x, y, y, align = align, padding = "0.2em")
, list_zip(xs, ys))

diagram(
    bar(xs, ys),
    annotations,
    width = 9,
    xaxis_subticks = "none"
)

Example: Climograph with Twin Axes

let months = ["Jan", "Feb", "Mar", "Apr", "May", "Jun", 
              "Jul", "Aug", "Sep", "Oct", "Nov", "Dec"]
let precipitation = [56, 41, 53, 42, 60, 67, 81, 62, 56, 49, 48, 54]
let temperature = [0.5, 1.4, 4.4, 9.7, 14.4, 17.8, 19.8, 19.5, 15.5, 10.4, 5.6, 2.2]
let xs = range(12)

diagram(
    yaxis(
        bar(xs, precipitation, fill = "blue.lighten(40%)", label = "Precipitation"),
        position = "right",
        axis_label = "Precipitation in mm"
    ),
    plot(xs, temperature, label = "Temperature", color = "red", stroke = "1pt", mark_size = 6),
    width = 8,
    title = "Climate of Berlin",
    ylabel = "Temperature in °C",
    xlabel = "Month",
    xaxis_ticks = months,
    xaxis_tick_rotate = -90,
    xaxis_subticks = "none"
)

Example: Koch Snowflake Fractal

// Complex number operations
define complex_add(c1, c2) = Pair(fst(c1) + fst(c2), snd(c1) + snd(c2))
define complex_sub(c1, c2) = Pair(fst(c1) - fst(c2), snd(c1) - snd(c2))
define complex_mul(c1, c2) = Pair(
    (fst(c1)*fst(c2)) - (snd(c1)*snd(c2)),
    (fst(c1)*snd(c2)) + (snd(c1)*fst(c2))
)

define triangle_vertex(angle) = Pair(cos(radians(angle)), sin(radians(angle)))
define base_triangle() = [triangle_vertex(90), triangle_vertex(210), triangle_vertex(330)]

define koch_edge(p1, p2) = 
    let d = complex_sub(p2, p1) in
    [p1, complex_add(p1, complex_mul(d, Pair(1/3, 0))),
     complex_add(p1, complex_mul(d, Pair(0.5, 0 - sqrt(3)/6))),
     complex_add(p1, complex_mul(d, Pair(2/3, 0)))]

define koch_iter(pts) = 
    let n = list_length(pts) in
    list_flatten(list_map(λ i . 
        koch_edge(list_nth(pts, i), list_nth(pts, mod(i + 1, n)))
    , range(n)))

let n0 = base_triangle()
let n3 = koch_iter(koch_iter(koch_iter(n0)))  // 192 vertices

diagram(
    path(n3, fill = "blue", closed = true),
    width = 6, height = 7,
    xaxis_ticks_none = true,
    yaxis_ticks_none = true
)

Example: Scatter Plot with Colormap

let xs = linspace(0, 12.566370614, 50)  // 0 to 4π
let ys = list_map(lambda x . sin(x), xs)
let noise = random_normal(50, 33, 0.1)
let xs_noisy = vec_add(xs, noise)
let colors = random(50, 42)

diagram(
    plot(xs, ys, mark = "none"),
    scatter(xs_noisy, ys, 
        mark = "s",
        colors = colors,
        map = "turbo",
        stroke = "0.5pt + black"
    ),
    theme = "moon"
)

Example: Stacked Area Chart

let xs = [0, 1, 2, 3, 4, 5, 6, 7, 8, 9]
let y1 = [0, 1, 3, 9, 5, 4, 2, 2, 1, 0]
let y2 = [5, 3, 2, 0, 1, 2, 2, 2, 3, 2]
let y3 = [0, 0, 0, 0, 1, 2, 4, 5, 5, 9]

diagram(
    stacked_area(xs, y1, y2, y3),
    theme = "moon"
)

Themes

Kleis supports Lilaq’s built-in themes:

diagram(
    plot(xs, ys),
    theme = "moon"
)

Axis Customization

Complete Example Notebook

Cell 1: Import stdlib

import "stdlib/prelude.kleis"

Cell 2: Generate data with linspace

let xs = linspace(0, 6.28, 50)
let ys = list_map(lambda x . sin(x), xs)

Cell 3: Plot with theme

diagram(
    plot(xs, ys, color = "blue", stroke = "2pt"),
    title = "Sine Wave",
    xlabel = "x",
    ylabel = "sin(x)",
    theme = "moon"
)

Logarithmic Scales

For exponential or power-law data, use logarithmic scales:

// Semi-log plot (linear x, logarithmic y)
diagram(
    plot([0, 1, 2, 3, 4], [1, 10, 100, 1000, 10000]),
    title = "Exponential Growth",
    yscale = "log"   // "linear", "log", or "symlog"
)

// Log-log plot (both axes logarithmic)
diagram(
    plot([1, 10, 100, 1000], [1, 100, 10000, 1000000]),
    title = "Power Law",
    xscale = "log",
    yscale = "log"
)

Available scales:

• "linear" - Default linear scale
• "log" - Logarithmic scale (base 10)
• "symlog" - Symmetric log (linear near 0, log elsewhere; handles negative values)

Next Steps

• Learn to create PDFs, theses, and papers: Document Generation
• Explore the REPL chapter for more interactive features
• See Matrices for symbolic matrix operations
• Check Z3 Verification for formal proofs