Show HN: Algebruh - Cross-check arithmetic claims with Z3, cvc5, and Lean

 (github.com)

13 points | by modinfo 19 hours ago

1 comments

  • derdi 3 hours ago
    Nice, but what is the motivation for this? That the syntax is perceived to be nicer than SMT-LIB format? Or that Lean can get involved? Differential testing? Just for fun?