4 ms·
What I mean is lean can prove things like one of cantors theorems, the proof of which requires you to derive from properties on a function f showing that there
by ratmice 3y ago
What I mean is lean can prove things like one of cantors theorems, the proof of which requires you to derive from properties on a function f showing that there exists a function g inverse to f, and show something about the results of calling g.
such a function in lean is considered non-computable by lean because it cannot be evaluated by lean since g has merely been shown to exist.
Many proofs in lean however are computable, just not all.
- westurner 3y agoI don't think SymPy has abstract Function attributes to reason about, but it does have limited reasoning about number classes given e.g. `x = Symbol('x', real=True)` SymPy docs > Writing Custom Functions > Easy Cases: Fully Symbolic or Fully Evaluated: https://docs.sympy.org/latest/guides/custom-functions.html#writing-custom-functions https://docs.sympy.org/latest/guides/custom-functions.html#w... If there is some sort of e.g. geometric correspondence, it could be possible for a Church-Turing classical computer to compute quantum functions (that return wave functions) that a Church-Turing-Deutsch quantum computer can compute; but otherwise Lean can't compute most quantum circuits either.