3 ms·

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 retur

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.

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.