Daniel Weber and Vlad Tsyrklevich: Equational Theories Proj

Stream: Lean Together 2025

[Riccardo Brasca]

A thread for discussion about this talk.

[Xavier Généreux]

Thank you for the talk!
There is mention of the convert tactic being too greedy in the talk.
Did you encounter this problem as well with convert h using 1 or convert h using 2 which caps the number of iterations of the congruence algorithm?

[Vlad Tsyrklevich]

The slides are here

[Daniel Weber]

Xavier Généreux said:

Thank you for the talk!
There is mention of the convert tactic being too greedy in the talk.
Did you encounter this problem as well with convert h using 1 or convert h using 2 which caps the number of iterations of the congruence algorithm?

When limiting the number of iterations sometimes it doesn't go deep enough

[Shreyas Srinivas]

Just a small correction. The project management stuff was designed by both me and Pietro

[Vlad Tsyrklevich]

Oops, apologies for getting that wrong!

[Shreyas Srinivas]

This is roughly where it began: #Equational > PRs Welcome : CI actions to manage the project @ 💬

[Shreyas Srinivas]

basically I set up the github project and designed the FSM and Pietro did the heavy lifting by writing the CI scripts to implement the FSM*. This was followed by several iterations of improvement.

*Finite State Machine

[Pietro Monticone]

:video_camera: Video recording: https://youtu.be/v_qL3Z_l47s?si=kKpBwtwkuJXDG44M

[Siddhartha Gadgil]

Thanks. I really enjoyed the talk.

I was wondering how deep is the integration of TPTP with Lean? Is there a type/typeclass/DSL in Lean for the TPTP format? Is there some mechanism to translate problems to TPTP if they are of the correct form?

[Vlad Tsyrklevich]

In Lean/Mathlib itself, there is no TPTP support as far as I'm aware. The Equational Theories Project translated from/to TPTP; however, I've also used Duper a bit and Duper does have some support for TPTP in Lean, like this. I'm not very familiar with what's there, so I'm not sure if you can translate _to_ TPTP, but clearly you can do some translation from TPTP as that example shows.

[Terence Tao]

Great talk and slides! I think many points from the slides could be incorporated into the paper (if they are not already there).