4 ms·

How about Lean? [0] There's a whole library of mathematics written down in Lean called Mathlib, which spans most of the undergraduate maths curriculum upto some

How about Lean? [0] There's a whole library of mathematics written down in Lean called Mathlib, which spans most of the undergraduate maths curriculum upto some cutting edge research-level maths. I've commented under the Part II post you linked to as well, describing how I think Mathlib could help the CAS ecosystem. [0] https://leanprover-community.github.io/ https://leanprover-community.github.io/

bmitc 3y ago
Mathlib is not nearly as complete as advertised. It is very much a collection of research projects with little cohesion.
- staunton 3y ago
  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?
  - deleted 3y ago
    [deleted]
staunton 3y ago
That's an entirely different thing though. Good luck getting Lean to help you do any symbolic computation whatever. You can use it to prove that a given manipulation is correct. You cannot use it to find a result (there may be a symbolic math library for Lean eventually but currently there isn't).
- viscousviolin 3y ago
  That's not my point. In the comment I made below the other post I talked about how Mathlib is just a piece of the puzzle, the way I see it [0]. I don't want to see Lean do symbolic computation - although I'm sure that would be great as well - what I want to see is to have Mathlib's library of mathematics being used in a way that any CAS can read definitions and theorems from it. Then a significant part of the CAS codebase won't have to be manually written, and developers can spend time on things that are not re-inventing some wheel. [0] https://news.ycombinator.com/item?id=37435449 https://news.ycombinator.com/item?id=37435449
  - deleted 3y ago
    [deleted]
  - staunton 3y ago
    Fair enough, that would be nice. However, it sounds like a very hard thing to build in practice. I'd expect, actually, it's best done in Lean itself. So you're proposing a CAS written in Lean, which noone is currently working on.
- logicchains 3y ago
  In Coq, the tactics system supports writing solvers than can both find a result and give you the proof that it's correct. If Lean also has a similar tactics system, then solvers could be written in that.
  - staunton 3y ago
    Lean does have a tactics system (very similar to Coq). However, there is no general tactic that will do, e.g., "sin^2 + cos^2 = 1" for you. (Writing a tactic specifically for that simplification is easy, of course, but that's not what a CAS is). (I doubt there is one in Coq that will do this, although I'm not sure). A symbolic algebra system is expected to do this simplification (and much more advanced ones) automatically. All in all, proof assistants aren't computer algebra systems. You could make computer algebra systems in those frameworks but I'm not aware of any.
    - zozbot234 3y ago
      Typically, there are 'group', 'ring' and 'field' tactics that will perform simplification in the relevant algebraic structures. Going from that to solving sin^2 x + cos^2 x is simply a matter of writing more such tactics, operating on e.g. real fields or whatever is applicable in any given case. This is a lot less ad-hoc than whatever CAS's do, but it's also less error prone.
      - westurner 3y ago
        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') or find_similar(expr, AxiomDB) would be useful. How do CAS differ from Production Rule Systems? https://en.wikipedia.org/wiki/Production_system_(computer_science) https://en.wikipedia.org/wiki/Production_system_(computer_sc... CAS > Simplification: https://en.wikipedia.org/wiki/Computer_algebra#Simplification https://en.wikipedia.org/wiki/Computer_algebra#Simplificatio... Rewriting: https://en.wikipedia.org/wiki/Rewriting https://en.wikipedia.org/wiki/Rewriting Because the rulesets are expected to change, rules engines have functionality to compile rules into a tree or better for performance. eBPF is not a rules engine, but it does optimize filter sets IIRC?

bmitc 3y ago

Mathlib is not nearly as complete as advertised. It is very much a collection of research projects with little cohesion.

staunton 3y ago
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?
- deleted 3y ago
  [deleted]

staunton 3y ago

That's an entirely different thing though. Good luck getting Lean to help you do any symbolic computation whatever. You can use it to prove that a given manipulation is correct. You cannot use it to find a result (there may be a symbolic math library for Lean eventually but currently there isn't).

viscousviolin 3y ago
That's not my point. In the comment I made below the other post I talked about how Mathlib is just a piece of the puzzle, the way I see it [0]. I don't want to see Lean do symbolic computation - although I'm sure that would be great as well - what I want to see is to have Mathlib's library of mathematics being used in a way that any CAS can read definitions and theorems from it. Then a significant part of the CAS codebase won't have to be manually written, and developers can spend time on things that are not re-inventing some wheel. [0] https://news.ycombinator.com/item?id=37435449 https://news.ycombinator.com/item?id=37435449
- deleted 3y ago
  [deleted]
- staunton 3y ago
  Fair enough, that would be nice. However, it sounds like a very hard thing to build in practice. I'd expect, actually, it's best done in Lean itself. So you're proposing a CAS written in Lean, which noone is currently working on.
logicchains 3y ago
In Coq, the tactics system supports writing solvers than can both find a result and give you the proof that it's correct. If Lean also has a similar tactics system, then solvers could be written in that.
- staunton 3y ago
  Lean does have a tactics system (very similar to Coq). However, there is no general tactic that will do, e.g., "sin^2 + cos^2 = 1" for you. (Writing a tactic specifically for that simplification is easy, of course, but that's not what a CAS is). (I doubt there is one in Coq that will do this, although I'm not sure). A symbolic algebra system is expected to do this simplification (and much more advanced ones) automatically. All in all, proof assistants aren't computer algebra systems. You could make computer algebra systems in those frameworks but I'm not aware of any.
  - zozbot234 3y ago
    Typically, there are 'group', 'ring' and 'field' tactics that will perform simplification in the relevant algebraic structures. Going from that to solving sin^2 x + cos^2 x is simply a matter of writing more such tactics, operating on e.g. real fields or whatever is applicable in any given case. This is a lot less ad-hoc than whatever CAS's do, but it's also less error prone.
    - westurner 3y ago
      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') or find_similar(expr, AxiomDB) would be useful. How do CAS differ from Production Rule Systems? https://en.wikipedia.org/wiki/Production_system_(computer_science) https://en.wikipedia.org/wiki/Production_system_(computer_sc... CAS > Simplification: https://en.wikipedia.org/wiki/Computer_algebra#Simplification https://en.wikipedia.org/wiki/Computer_algebra#Simplificatio... Rewriting: https://en.wikipedia.org/wiki/Rewriting https://en.wikipedia.org/wiki/Rewriting Because the rulesets are expected to change, rules engines have functionality to compile rules into a tree or better for performance. eBPF is not a rules engine, but it does optimize filter sets IIRC?