GEgeckones·Jul 5, 2026
The developer here! Thanks for all the feedbacks, here are some more info
There is a tutorial: https://dhilst.github.io/algae
The project (algae) is a algebraic specification tool. This means it is intended to allow you to write algebraic specs, in which you define your data types (sorts), operations (ops), and the the equations chatacterizing the operations (axioms). It is a formal specification technique. I designed because I want something to pratice/improve my proof theory skills, so, distinct from Lean4 or Roqc, all the proof information is visible in the surface syntax, but it still lack ergonomics.
About the tutorial and the game, I want it to be "proof theory introction"-like but the generated proofs are really not as good as I want they to be. The dificult progressions does not exist, the help sometimes does not help, some lemmas
Read the rest
provide the proof in their arguments. To fix that I will need to go proof by proof and fix the help manually and also work on the progression. The AI is terrible at generating the proofs (yes it was made with AI help but I have formal specs experience).
About the game, it may still be buggy, feel free to open issues at https://github.com/dhilst/algae/issues, and I will fix it. I want to provide a cool playground for ppl to learn proof theory and for me to pratice it too.