Towards a new SymPy

Post by staunton » Mon, Sep 11, 2023, 9:49 AM UTC

westurner wrote: post #70

staunton wrote: post #57

Earlier quoted context omitted.

Julia's Symbolics.jl allows users to easily add custom rewrite rules. However, it's not a state-of-the-art CAS. I don't have that much experience with others. Mathematica doesn't allow it, I think.

FWIU Wolfram's searching for a unified model with the Wolfram Physics Project, too; e.g. "The Physicalization of Metamathematics and Its Implications for the Foundations of Mathematics" (2022) https://www.wolframscience.com/metamathematics/ https://www.wolframphysics.org/bulletins/ Are fundamental constants other-valued in any Many Worlds interpretations, or are e, i, and Pi always e, i, and pi with the same relation…

I don't see how that relates to the question of "does Mathematica allow users to define simplification rules?"

Post by westurner » Wed, Sep 20, 2023, 7:04 PM UTC

staunton wrote: post #71

westurner wrote: post #70

Earlier quoted context omitted.

FWIU Wolfram's searching for a unified model with the Wolfram Physics Project, too; e.g. "The Physicalization of Metamathematics and Its Implications for the Foundations of Mathematics" (2022) https://www.wolframscience.com/metamathematics/ https://www.wolframphysics.org/bulletins/ Are fundamental constants other-valued in any Many Worlds interpretations, or are e, i, and Pi always e, i, and pi with the same relation…

I don't see how that relates to the question of "does Mathematica allow users to define simplification rules?"

https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_g... :

> In this game, you get own version of the natural numbers, called `mynat`, in an interactive theorem prover called Lean. Your version of the natural numbers satisfies something called the principle of mathematical induction, and a couple of other things too (Peano's axioms).

Such axioms are hard-coded in SymPy, SageMath, and Mathematica but not in Lean Mathlib (which is not optimized for performance)

If there are an infinite number of unitary transformations (as rotations on a Bloch sphere for example), I find it unlikely that we've yet discovered all of the requisite operators and axioms and coded them into any human CAS that exists in present day.

Re: Towards a new SymPy

Re: Towards a new SymPy