# mathematics
# subtopics
~~~
%scm link-files "textual/more/mathematics/*"
~~~

# links
## mathematics at the computational frontier
* [Lean + mathlib](https://leanprover-community.github.io/) a modern interactive theorem prover with a growing standard library; widely used for formalizing real mathematics and increasingly integrated with AI tools
* [Coq](https://coq.inria.fr/) a mature proof assistant based on constructive type theory; used for certified software (e.g. CompCert) and foundational mathematics
* [Z3 (SMT Solver)](https://github.com/Z3Prover/z3) a high-performance satisfiability modulo theories solver; used in program analysis, formal verification, and backend automation in proof systems
* [Homotopy Type Theory (HoTT)](https://homotopytypetheory.org/) a new foundation for mathematics using higher-dimensional types; encodes structure-sensitive equality via paths and supports univalent reasoning
* [Metamath](https://us.metamath.org/) an ultra-minimal formal system for expressing all of mathematics using explicit substitution; emphasizes kernel transparency and syntactic traceability
* [Lean-GPT / TheoremTactic](https://arxiv.org/abs/2107.03374) AI-driven tools for formal proof suggestion and tactic synthesis; integrate language models with proof assistants to assist and accelerate formalization

## wikipedia
* [algebra](https://en.wikipedia.org/wiki/Algebra)
* [arithmetic](https://en.wikipedia.org/wiki/Arithmetic)
* [geometric algebra](https://en.wikipedia.org/wiki/Geometric_algebra)
* [golden ratio](http://en.wikipedia.org/wiki/Golden_ratio)
* [linear algebra](https://en.wikipedia.org/wiki/Linear_algebra)
* [linear interpolation](https://en.wikipedia.org/wiki/Linear_interpolation)
* [list of mathematical constants](https://en.wikipedia.org/wiki/List_of_mathematical_constants)
* [list of types of numbers](https://en.wikipedia.org/wiki/List_of_types_of_numbers)
* [mathematical constant](https://en.wikipedia.org/wiki/Mathematical_constant)
* [mathematical proof](https://en.wikipedia.org/wiki/Mathematical_proof)
* [outline of mathematics](https://en.wikipedia.org/wiki/Outline_of_mathematics)
* [plastic number](https://en.wikipedia.org/wiki/Plastic_number)
* [proof that 0.999... equals 1](http://en.wikipedia.org/wiki/Proof_that_0.999..._equals_1#Proofs)
* [property](https://en.wikipedia.org/wiki/Property_(mathematics))
* [timeline of mathematics](https://en.wikipedia.org/wiki/Timeline_of_mathematics)

## other
* [online encyclopedia of integer sequences](https://oeis.org/)
* [mathsisfun.com](https://www.mathsisfun.com/)
* [math-as-code](https://github.com/Experience-Monks/math-as-code)
* [normal distribution](http://www.mathsisfun.com/data/standard-normal-distribution.html)
* [natural number game](https://adam.math.hhu.de/#/g/leanprover-community/nng4)
* [linear algebra done right](https://linear.axler.net/)
* [mathgen](http://thatsmathematics.com/mathgen) generate random mathematics research papers
* [list of math formulas](https://www.matematica.pt/en/useful/math-formulas.php)

# 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.