Is there a most flexible type theory or proof assistant?

Question

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?

Answer 1

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.

Answer 2

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.