2025-11-23

mathematics

subtopics

geometric algebra

n-cubes (hypercubes)

opaque math notations

outline of mathematics

links

mathematics at the computational frontier 2025

  • 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

on the differences between mathematics and computer science

if computer science were primary and mathematics emerged later, the distinguishing features of mathematics would be:

  • systematic minimization of operational detail
  • pursuit of invariant structure independent of representation
  • explicit separation of syntax from semantics
  • construction of theories where all permissible transformations are closed under a small set of axioms
  • maximal generalization such that the same formal object applies across many computational regimes
  • preference for proofs that eliminate reliance on procedural execution
  • focus on completeness, consistency, decidability, and other global properties not tied to any particular computational model

in such a sequence, mathematics would appear as a discipline that abstracts away from machines, encodings, and resource bounds, producing structures that unify rather than implement. it would specialize in identifying the minimal information required for a property to hold, and in characterizing spaces of possible computations rather than any concrete computation itself.