Axiomagic.fun - math resources

Math Topics

pragmatism, logic, and categories
programs, types and proofs
distributed state machines
probability monads
example: physics formalization
example: finance formalization

Background Sources

These links will open in new window. Citations after this section open in-page when possible.

(SEP) Stanford Encyclopedia of Philosophy
- See also Visualizing SEP graph browser UI, by Joseph DiCastro
(ISKO) International Society for Knowledge Organization
(KBP) KBPedia integrated upper ontology reference
(LML) Lean MathLib
treated as a library of math element types
(nLab) (nCatLab.org by Urs Schreiber et. al.),
treated as a structured, informal glossary of categorical math concepts.
Concept terms in the nLab vocabulary may be tried as query terms in an AxioMagic browser.
(OutRect) Stu B22's tech blog

pragmatism, logic, and categories

Hierarchy (ISKO) incl "A typology of knowledge system hierarchies"
Pragmatism (SEP) our big picture humanist why
Intensional Logic (SEP)
Category Theory (SEP)

programs, types and proofs

Type Theory (SEP) - general treatment suitable for review, not really for introduction
Intuitionistic Type Theory (SEP)

distributed state machines

Physically, digital states may be thought of as structures containing unsigned integers

probability monads

Composed Stochastic Proof (blog entry)
Domain types based on probability monads (blog entry)

physics formalization approach

Builds on category theory and math formalization resources.
User models knit together background definition sources like Wikipedia, nLab, Lean/Agda libs in interactive knowledge views

nLab (ncatlab.org)
- nLab main topics in iframe below (47 terms)
- nLab all pages in new window (15670 terms)

financial formalization approach

FIBO is a rich set of open vocabularies for financial transactions alignment, available in RDF + URI form.
User calculations using URI-resolved input data may have URI-aligned meanings in results.
Distributions of asset returns are expressable as composed monads over aligned models and datasets.
User finds/uses/makes proofs about these distributions.