fricas and lean (theorem prover)

[Qian Yun]

https://github.com/DustinTheismann/omniforge/pull/2

This seems to be an interesting project, that bridges
CAS and theorem prover -- it seems to do verification
of integrals.

I haven't digged deeper, but this formulation of Category
(catdef.spad) in Lean looks especially interesting to me.

https://github.com/DustinTheismann/omniforge/commit/376bb7c1bd01afe3e9623f5957849a4f91c6689c

This project seems to be heavily AI assisted.

- Qian

[Tim Daly]

You might want to look at this video

https://www.youtube.com/watch?v=bSDkbx5rrpM

I suspect it is possible to ask the AI about building an

MCP server for computer algebra. Then the AI can use

the computer algebra to do things like integration.

Tim