Sylvester: Unified, typed, notation for symbolic mathematics and proofs (short talk)
summary
Claim: F# becomes a single interactive language that unifies computer algebra and theorem proving. Built is the Sylvester library running in Jupyter/VS Code that uses F# quotations as the symbolic syntax, delegates CAS work to Maxima and SMT/solving to Z3, implements an LCF-style equational prover and a term datatype type-level vector dimensions so non‑conformable matrix ops fail at compile time; examples run and Z3 finds unsat/counterexamples.
AI-written summary · about