My understanding is that a programming language designed for “doing math” would basically:

  1. Be able to represent mathematical ideas (hopefully in a similar way to non-programmatic mathematical notation)
  2. Have some kind of transformation rules relating changes in the form of an expression to ideas of valid “logical inference”

To me this makes me imagine such a language could be used for meta-programming, like, for any expression, I can apply some rule / function to transform the function into a new, valid form.

I suppose that in the same way, it can act as a proof-checker, maybe if parsing a series of expressions or “executing” it just results output of whether or not it was “executable”.

I guess I am curious to know about how this works, what goes on under the hood?

I’ve read around and it seems like people talk about how each language like Agda or Coq or Lean has its own particularities, assumptions it has made about what type theory or kind of set theory it is based on, what axioms it assumes.

But ideally, is there any type system, in view of modern mathematical attempts to view all such systems abstractly, which underlies all such choices? Like a most flexible or foundational proof assistant language / type theory?

Which type theory is that?

And, is there a programming language which uses it? If not, why not?

  • 2
    $\begingroup$ It would help to know a bit about your background. Also, have you looked at any of the major proof assistants? $\endgroup$ Jun 6 at 11:45
  • 1
    $\begingroup$ Maybe this too github.com/fizruk/rzk $\endgroup$
    – Julius H.
    Jun 7 at 19:56
  • 1
    $\begingroup$ I glad to see that Google solved your problems. You should be in good hands at agda-unimath. $\endgroup$ Jun 7 at 21:25
  • 1
    $\begingroup$ @hmltn I'm sorry, what is your ultimate question? "What is the most foundational type theory that forms true basis of all of mathematics?" Or "why there's no such type theory and no such proof assistant?" $\endgroup$ Jun 8 at 14:09
  • 1
    $\begingroup$ This question is without focus. Is there a specific point about proof assistants that we can address? Just piling on links to various results about incompleteness isn't really contributing anything. My impression is that you're on a fishing expedition, except you're trying to catch knowledge instead of fish. In that case, this isn't the right forum. Something like the Lean, Coq, Agda, category theory Zulip instances would provide better feedback. $\endgroup$ Jun 24 at 8:20

2 Answers 2


If you are asking whether there is "one type system which rules them all", then the answer is negative.

By classic results of 20th century logic, and Kurt Gödel in particular, there can never be a single mathematical formalism that encomapsses all of mathematics.

  • $\begingroup$ Thank you. And is there a strong implication of that, in this context? For example, if there cannot be a type theory to formalize all others in, does that make it impossible to mathematically organize various type theories schematically into relationships with one another, or for us to ever predict what new type theories are possible? Is it somehow implying an infinitude of different possible mathematical systems with no unifying principles beneath them all? $\endgroup$
    – Julius H.
    Jun 23 at 14:14
  • 2
    $\begingroup$ You are making a mistake of the kind "there is no fastest car, therefore traffic is impossible". $\endgroup$ Jun 23 at 20:31
  • $\begingroup$ There is no total ordering on the relation between type theories to one another, but partial orderings, local relationships, etc.? But do you find we must confront this dichotomy: either there is a system which can be used to express all the various type theories and their relationships to one another, or there isn’t. If there is, we have a universal foundation. If there isn’t, we have an inability to talk about a “totality of type theories” in a useful, general way. Could there be a boundary between a philosophical characterization of “all type theories” (like, a “collection”), and $\endgroup$
    – Julius H.
    Jun 24 at 7:26
  • $\begingroup$ an extremely flexible, very tenuously defined mathematical system, like quasicategories? $\endgroup$
    – Julius H.
    Jun 24 at 7:27
  • $\begingroup$ I would like to add, in what way are univalent foundations univalent regarding the incompleteness theorem? $\endgroup$
    – Julius H.
    Jun 24 at 7:31

I'm new to Lean but am coming from a Physics background. Mathematical Physics relies on derivations comprised of steps. The steps relate expressions using inference rules. For example, oscillatory period is the inverse of oscillatory frequency: $$T = 1/f$$ This equation is related to $T f = 1$ by the inference rule "multiply both sides by __". In this step __ is $f$.

The concept of inference rules for derivations is not specific to mathematical Physics. Inference rules apply to mathematical derivations as well.

Inference rules in derivations are, for specific equations, provable using proof assistants like Lean. While Lean cannot prove an inference rule like "multiply both sides by __" we can use Lean to prove the application of the inference rule to equations like $$(T=1/f) \rightarrow (T f=1)$$

The reason an inference rule like "multiply both sides by __" isn't provable in Lean is because it lacks the specificity of types. Is the __ Real? Complex? Do the predicate equations and goal equations contain Real or Complex values? Matrices?

I've cataloged inference rules commonly used in Physics here and am planning to prove each application using Lean.

  • 1
    $\begingroup$ Tiny nitpick: That inference is false in lean because of division by zero. But if you add $f \ne 0$ you'll be fine. $\endgroup$
    – Trebor
    Jun 19 at 3:48

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.