gpt-3

input

Here is the "set theory" language:
type Set
type Point
type Map

constructor Singleton : Point p -> Set

function Intersection : Set a * Set b -> Set
function Union : Set a * Set b -> Set
function Subtraction : Set a * Set b -> Set
function CartesianProduct : Set a * Set b -> Set
function Difference : Set a * Set b -> Set
function Subset : Set a * Set b -> Set
function AddPoint : Point p * Set s1 -> Set

predicate Not : Prop p1
predicate From : Map f * Set domain * Set codomain
predicate Empty : Set s
predicate Intersecting : Set s1 * Set s2
predicate IsSubset : Set s1 * Set s2
predicate PointIn : Set s * Point p
predicate In : Point p * Set s
predicate Injection : Map m
predicate Surjection : Map m
predicate Bijection : Map m
predicate PairIn : Point * Point * Map

notation "A ⊂ B" ~ "IsSubset(A, B)"
notation "p ∈ A" ~ "PointIn(A, p)"
notation "p ∉ A" ~ "PointNotIn(A, p)"
notation "A ∩ B = ∅" ~ "Not(Intersecting(A, B))"
notation "f: A -> B" ~ "Map f; From(f, A, B)"

Here is an example of the "set theory" language:
Set A
Set B
Set C
Set D
Set E
Set F
Set G
IsSubset(B, A)
IsSubset(C, B)
IsSubset(D, C)
IsSubset(E, D)
IsSubset(F, E)
IsSubset(G, F)

---

Here is the "linear algebra" language:

type Scalar
type VectorSpace
type Vector
type LinearMap


function neg: Vector v -> Vector
function scale: Scalar c * Vector v -> Vector cv
function addV: Vector * Vector -> Vector
function addS: Scalar s1 * Scalar s2 -> Scalar
function norm: Vector v -> Scalar
function innerProduct: Vector * Vector -> Scalar
function determinant: Vector * Vector -> Scalar
function apply: LinearMap f * Vector -> Vector


predicate In: Vector * VectorSpace V
predicate From: LinearMap V * VectorSpace domain * VectorSpace codomain
predicate Not: Prop p1
predicate Orthogonal: Vector v1 * Vector v2
predicate Independent: Vector v1 * Vector v2
predicate Dependent: Vector v1 * Vector v2
predicate Unit: Vector v


notation "det(v1, v2)" ~ "determinant(v1, v2)"
notation "LinearMap f : U → V" ~ "LinearMap f; From(f, U, V)"
notation "v1 + v2" ~ "addV(v1, v2)"
notation "-v1" ~ "neg(v1)"
notation "Vector a ∈ U" ~ "Vector a; In(a, U)"
notation "|y1|" ~ "norm(y1)"
notation "<v1,v2>" ~ "innerProduct(v1, v2)"
notation "s * v1" ~ "scale(s, v1)"
notation "Scalar c := " ~ "Scalar c; c := "
notation "f(v)" ~ "apply(f, v)"

Here is an example of the "linear algebra" language:
VectorSpace V

result

VectorSpace W
LinearMap f : V → W
Vector v1 := Vector(2, 1)
Vector v2 := Vector(3, 0)
Dependent(v1, v2)
Independent(v1, v2)
Orthogonal(v1, v2)

slightly better result:

Vector u ∈ V
Vector v ∈ V
Vector w ∈ V
Scalar s1, s2 ∈ V
LinearMap f : U → V
Independent(u, v)
Dependent(v, u)
Orthogonal(u, v)
Unit(u)