Others
Arity
In logic, mathematics, and computer science, thearity of a function or operation is the number of arguments or operands that the function takes. In mathematics, arity may also be namedrank, but this word can have many other meanings in mathematics. In logic and philosophy, it is also calledadicityanddegree.In linguistics, it is usually named valency.
https://en.wikipedia.org/wiki/Arity
Category Theory
Category theory formalizes mathematical structure and its concepts in terms of a labeled directed graph called a category, whose nodes are called objects, and whose labelled directed edges are called arrows(or morphisms). A category has two basic properties: the ability to compose the arrows associatively and the existence of an identity arrow for each object. The language of category theory has been used to formalize concepts of other high-level abstractions such as sets, rings, and groups
Category theory has practical applications in programming language theory, for example the usage of monads in functional programming. It may also be used as an axiomatic foundation for mathematics, as an alternative to set theory and other proposed foundations.
https://en.wikipedia.org/wiki/Category_theory
Orthogonality
In mathematics, orthogonalityis the generalization of the notion of perpendicularity to the linear algebra of bilinear forms. Two elementsuandvof a vector space with bilinear formBareorthogonalwhenB(u, v) = 0. Depending on the bilinear form, the vector space may contain nonzero self-orthogonal vectors. In the case of function spaces, families of orthogonal functions are used to form a basis. By extension, orthogonality is also used to refer to the separation of specific features of a system. The term also has specialized meanings in other fields including art and chemistry.
https://en.wikipedia.org/wiki/Orthogonality
Tools
Lean Theorem Prover
Lean 4 programming language and theorem prover
Lean is a functional programming language that makes it easy to write correct and maintainable code. You can also use Lean as an interactive theorem prover. Lean programming primarily involves defining types and functions. This allows your focus to remain on the problem domain and manipulating its data, rather than the details of programming.
https://github.com/leanprover/lean4
https://leanprover.github.io/about