4 ms·
The existence of https://github.com/robertylewis/mathematica https://github.com/robertylewis/mathematica makes me think it's more likely to go in the other dire
by Smaug123 4y ago
The existence of https://github.com/robertylewis/mathematica https://github.com/robertylewis/mathematica makes me think it's more likely to go in the other direction, where you treat powerful tools as untrusted oracles which produce certificates that Lean then verifies.
- zozbot234 4y agoSure that's possible, but "untrusted oracles" are only useful if they provide easily-verified certificates. Some CAS problems are amenable to that approach, but not all. There's no difference in this case between Mma and, e.g. an external SAT/SMT solver.