The group has the express goal of finding ways in which current computer algebra systems can interact with formal theorem provers, such as Lean, and vice versa.

The group has the express goal of finding ways in which current computer algebra systems can interact with formal theorem provers, such as Lean, and vice versa. The guiding motivation for this project is to discuss to what extent Lean should operate as a CAS in it's own right. This groups concrete goals could be anything from the actual development of CAS technology in Lean, or could be to create an argument about the extent to which Lean should be used as a computer algebra system at all. The primary focus of this group should be to decide to what extent these mathematical technologies should mix and to come up with ways to implement these solutions.