61–70 of 72 posts
Earlier quoted context omitted.
Mathlib is not nearly as complete as advertised. It is very much a collection of research projects with little cohesion.
A CAS also covers only a tiny part of "an undergrad math degree" so that's beside the point here. Assuming it had appropriate tactics doing the job of a CAS using all theorems (which isn't happening any time soon), what math would be missing?
I remember being a kid and fawning over the upgrade from a TI-86 (which could not do symbolic manipulation) to the TI-89 (which could). As an adult and OSS enthusiast, I've often wondered if there is an OSS option that can at least match, and ideally exceed, the TI-89's capabilities. Is SymPy it? I've had a few reasonably good experiences with SymPy, but I don't know much about the theoretical underpinnings of CAS, o…
Depends what you mean? Mathematica is quite impressive. Many symbolic options exist in lisps. https://stackoverflow.com/questions/10355112/why-is-lisp-so-... is a good answer that goes over some of the reason for that.
Earlier quoted context omitted.
Depends what you mean? Mathematica is quite impressive. Many symbolic options exist in lisps. https://stackoverflow.com/questions/10355112/why-is-lisp-so-... is a good answer that goes over some of the reason for that.
Mathematica is certainly as powerful as a TI-89, but not OSS.
I'm sure there are restrictions, but likely not a concern for hobby interests?
Earlier quoted context omitted.
It's true. Unfortunately Mathematica simply can't be used in many domains. I would really like to integrate mathematica with a type checker for automatic theorem proving. I think it could greatly alleviate the clunkiness of dependent types.
What's preventing it from being used?
Earlier quoted context omitted.
What's preventing it from being used?
I can hardly accept a cool $3230 per year license. I didn't even attempt to go this route. I doubt they would even allow it tbh. The site isn't exactly clear on that.
Earlier quoted context omitted.
I can hardly accept a cool $3230 per year license. I didn't even attempt to go this route. I doubt they would even allow it tbh. The site isn't exactly clear on that.
I thought you meant "domain" like a field of work or study.
Earlier quoted context omitted.
Yes type checkers are a domain of study. Basically any domain where mathematica needs to integrated into the end result as is.
Implying there's a technical reason it couldn't be used.
If a company simply blocks you from using their tech that definitely means you can't use it. For example. I can't run my own entertainment system on a Tesla car. There is no technical reason it's not possible. Tesla simply disallows it.
Earlier quoted context omitted.
Implying there's a technical reason it couldn't be used.
I wasn't implying there is a technical reason, I definitely didn't mean it that way. If Mathematica were open sourced tomorrow nothing would stand in the way of trying it out. If a company simply blocks you from using their tech that definitely means you can't use it. For example. I can't run my own entertainment system on a Tesla car. There is no technical reason it's not possible. Tesla simply disallows it.
Earlier quoted context omitted.
Do any existing CAS systems have configurable axioms? OTOH: Conway's surreal infinities, Do not early eliminate terms next to infinity, Each instance of infinity might should have a unique identity, configurable Order of operations, All of the axiomatic transformations applied by a CAS like SymPy should/must be in Lean Mathlib somewhere? If nothing else, a lookup_lean_mathlib_definition(expr, 'path/to/mathlib-v0.0.2'…
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.
Are fundamental constants other-valued in any Many Worlds interpretations, or are e, i, and Pi always e, i, and pi with the same relations?
Countability and continuua (in a Hilbert space of degree n, where n is or is not inconstant like the many forms of [quantum discord] entropy and the energy that represents them)
TIL the separable states problem is considered NP-hard, and many models specify independence of observation as necessary.