2025-08-01

mathematics

subtopics

geometric algebra a collection of links and notes of varying quality.

n-cubes notes and information about n-cubes that i could not find summarized in other places.

opaque math notations here are several categories of mathematical notation that are especially opaque or hard to track for someone from a computer science background, along with illustrative examples. these represent excellent test cases for stress-testing a referential, programming-inspired notation.

overview of mathematical structures

referential math notation (rmn) specification an ascii plaintext math notation

links

mathematics at the computational frontier

  • Lean + mathlib a modern interactive theorem prover with a growing standard library; widely used for formalizing real mathematics and increasingly integrated with AI tools
  • Coq a mature proof assistant based on constructive type theory; used for certified software (e.g. CompCert) and foundational mathematics
  • Z3 (SMT Solver) a high-performance satisfiability modulo theories solver; used in program analysis, formal verification, and backend automation in proof systems
  • Homotopy Type Theory (HoTT) a new foundation for mathematics using higher-dimensional types; encodes structure-sensitive equality via paths and supports univalent reasoning
  • Metamath an ultra-minimal formal system for expressing all of mathematics using explicit substitution; emphasizes kernel transparency and syntactic traceability
  • Lean-GPT / TheoremTactic AI-driven tools for formal proof suggestion and tactic synthesis; integrate language models with proof assistants to assist and accelerate formalization

wikipedia

other

five important generalizations in mathematics

  • group theory generalizes algebraic operations by abstracting the notion of symmetry and invertible structure.
  • topology generalizes geometry by focusing on continuity and qualitative spatial properties rather than metric or angle.
  • measure theory generalizes length, area, and volume in a rigorous way, enabling integration beyond riemann sums.
  • category theory generalizes mathematical structures and functions via objects and morphisms, unifying various branches.
  • functional analysis generalizes linear algebra and calculus to infinite-dimensional vector spaces.