@Lasse recently presented his work on Tactician at CICM 2020, which triggered questions from @brando90 (Gitter import) in the CICM 2020 Slack and now on Discourse. Looking at these discussions and also the comparisons with all the other ML works like CoqGym and the other related works on hammers (CoqHammer), I was thinking that it might make sense to start a Zulip stream on these topics (tentatively titled "AI and hammers devs & users") so that the informal discussion can continue. What do you think @Lasse (and also @Emilio Jesús Gallego Arias, @Karl Palmskog, @Łukasz Czajka...)?
I agree something like this would be useful. But I personally don't like the "AI" label (it's short, but "machine learning" is better)
maybe: "machine learning and (proof) automation". ML bound to be confused with OCaml/SML
I was joking :-)
We should set up an elaborate scam to convince venture capitalists that "ML" meant meta-language all along, and extract as much money as possible from it for PLT research...
Sounds good! I also prefer the term machine learning over AI :-) Regarding my tool: Tactician is not quite ready for mass adoption by end-users yet (I've not made a 1.0 release and it's not yet in the opam repo). That being said, if there are people who would like to give some feedback, that would be appreciated. That mainly regards the user experience, such as installation and learning from libraries (standard libraries and others). Regarding its strength: My guess is that the current learner is not yet good enough to be massively useful. I'm currently working on improvements, which I expect will land in a couple of weeks. Installation instructions can be found at coq-tactician.github.io
This topic was moved by Théo Zimmermann to #Machine learning and automation > Comparative evaluation
Last updated: Aug 14 2022 at 13:02 UTC