6 ms·

Not all lean proofs are actually computable, see the computable function link in the url you gave.

westurner 3y ago
Not all code functions are mathematical functions. An expression can describe a relation that is not a function per the definition like "a function always returns one output for one input". Function (mathematics) https://en.wikipedia.org/wiki/Function_(mathematics) https://en.wikipedia.org/wiki/Function_(mathematics) The Navier-Stokes equations are PDEs, not functions; but are they computable in Lean, or can algorithms for finding solutions be expressed in Lean? Lean docs > Missing undergraduate mathematics in mathlib: https://leanprover-community.github.io/undergrad_todo.html#:~:text=Multivariable%20calculus https://leanprover-community.github.io/undergrad_todo.html#:... Is ℯ^(2ί π x) a function? It's a complex function, but Geogebra draws it as a ~ (unit circle) + (y=0 if x > 0).
- 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 ago
    I 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.

Not all code functions are mathematical functions. An expression can describe a relation that is not a function per the definition like "a function always returns one output for one input". Function (mathematics) https://en.wikipedia.org/wiki/Function_(mathematics) https://en.wikipedia.org/wiki/Function_(mathematics) The Navier-Stokes equations are PDEs, not functions; but are they computable in Lean, or can algorithms for finding solutions be expressed in Lean? Lean docs > Missing undergraduate mathematics in mathlib: https://leanprover-community.github.io/undergrad_todo.html#:~:text=Multivariable%20calculus https://leanprover-community.github.io/undergrad_todo.html#:... Is ℯ^(2ί π x) a function? It's a complex function, but Geogebra draws it as a ~ (unit circle) + (y=0 if x > 0).

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 ago
  I 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.