Data
The Data panel keeps exact values next to your lesson. It computes with Lean's own rules, and Lean can check the answers.
Each lesson has its own values.
Type a value
| Type | Gets |
|---|---|
5/6 0.75 |
numbers (0.75 is exactly 3/4) |
3 mod 7 |
a residue in ℤ/7ℤ |
2 + i |
a Gaussian integer |
1 2; 3 4 |
a matrix |
(0 1 2)(2 3) |
a permutation |
Compute
| Type | Gets |
|---|---|
A * B A⁻¹ A.det |
products, inverses, determinants |
C := A * B |
a result with a name |
x ^ 6 = 1 |
a statement: Check says if it is true |
Lean's rules
- A number with no type is natural:
7 / 2is3,3 - 5is0. - Write
(7 : ℚ) / 2for the fraction. - Permutations compose right to left.
Where Lean comes in
The app computes, exactly and at once. Lean checks.
- Check in Lean, on a result: Lean computes it too, and the two are compared.
- Prove in Lean, on a true statement: Lean proves it, and its kernel checks the proof.
- A name the app does not know, such as
Nat.choose 10 3, goes to Lean by itself. That takes about three seconds, and the result says Lean computed it.
Where there is no answer, the app says why and does not ask Lean: 2 has no inverse in ℤ/4ℤ.
The Python button hands your values to SymPy.
For agents
The assistant uses data_reference, data_read, data_add and
data_compute. This is what it reads:
The data panel: named, typed values beside the lesson, computed exactly by the app, with Lean's semantics. In the panel, Lean computes what the app does not know, and checks or proves a result when the reader asks.
Values (data_add {"name", "value", "kind"?}; kind is guessed when omitted):
- 5/6 0.75 -3: numbers: 0.75 is exactly 3/4
- 3 mod 7: a residue in ℤ/7ℤ
- 2 + i 1 + 2i + 3j + 4k: a Gaussian integer, a quaternion
- 1 2; 3 4: a matrix: spaces between entries, ; between rows
- (1, 2, 3) [3, 1, 2]: a vector, a list
- (0 1 2)(2 3): a permutation in cycles, composed right to left Kinds: natural, integer, rational, float, zmod (give "n"), gaussian, quaternion, matrix / vector / list (give "over": rational, integer, natural, float or zmod), permutation (give "n"), boolean.
Computations (data_compute {"expr", "name"?}), with the values by name:
- A * B A⁻¹ Aᵀ A.det x ^ 6: compute: products, inverses, transposes, powers
- C := A * B: compute, and name the result
- x ^ 6 = 1 A * B = B * A: a proposition: Check it, then Prove in Lean
- Nat.Prime n Nat.primeFactorsList n: whole numbers: primes, factors
- Nat.factorial n Nat.fib n Nat.gcd a b: factorials, Fibonacci, gcd and lcm
- (7 : ℚ) / 2 (n : ℤ) - 20: a type for a number: with none, it is ℕ, as in Lean Functions: det, transpose (or ᵀ), trace, inv (or ⁻¹), sign, orderOf, star (conjugate), norm, length, Nat.Prime, Nat.primeFactorsList, Nat.totient, Nat.factorial, Nat.fib, Nat.gcd a b, Nat.lcm a b, l.sum, l.prod, l.reverse; as methods too (A.det, n.Prime).
Lean's rules, which the panel keeps: a number with no type is ℕ, so 7 / 2 is 3 and 3 - 5 is 0; write (7 : ℚ) / 2 or (3 : ℤ) - 5. A numeral beside a square matrix is a multiple of the identity (A + 1). Permutations compose right to left. Floats round: compare exact values in ℚ.