Zulip Chat Archive

Stream: new members

Topic: Is `simp` an AI?


view this post on Zulip Huỳnh Trần Khanh (Feb 09 2021 at 08:38):

Is simp an AI? Why does @Kevin Buzzard describe it as an AI? What machine learning (or not) algorithm does it use? Why is it faster than library_search? To me simp is the best thing since sliced bread, Dafny tries to close every induction-ish goal but doesn't give me much control over the process but in Lean I can write the outline of the induction proof, throw simp at it and move on while I retain fine-grained control!

view this post on Zulip Johan Commelin (Feb 09 2021 at 08:40):

simp is a rewriting system. It doesn't use any machine learning. Whether it's an AI depends on what your defn of AI is.

view this post on Zulip Huỳnh Trần Khanh (Feb 09 2021 at 08:42):

So how does it work internally then? Where can I read more about it?

view this post on Zulip Johan Commelin (Feb 09 2021 at 08:42):

It is clearly intelligent. Whether it's artificial...

view this post on Zulip Johan Commelin (Feb 09 2021 at 08:43):

https://en.wikipedia.org/wiki/Rewriting

view this post on Zulip Patrick Massot (Feb 09 2021 at 08:56):

https://leanprover-community.github.io/extras/simp.html

view this post on Zulip Eric Wieser (Feb 09 2021 at 08:58):

Has @Kevin Buzzard's rewrite of that document been merged yet?

view this post on Zulip Patrick Massot (Feb 09 2021 at 08:59):

yes

view this post on Zulip Patrick Massot (Feb 09 2021 at 09:00):

But then I censored his innovation of "smip normal fomr".

view this post on Zulip Kevin Buzzard (Feb 09 2021 at 09:03):

I thought "AI" was just any algorithm which attempts to solve a problem. I am not a computer scientist -- feel free to correct the document!

view this post on Zulip Eric Wieser (Feb 09 2021 at 09:09):

I assume simp is just a greedy algorithm, so calling it AI would be quite a stretch

view this post on Zulip Kevin Buzzard (Feb 09 2021 at 09:10):

I call refl an AI.

view this post on Zulip Jasmin Blanchette (Feb 09 2021 at 09:19):

Just like you guys distinguish between elementary math and advanced math, we have non-AI vs. AI. It can't be defined, but if there's not a substantial heuristic / ad hoc component, it's not an AI.

view this post on Zulip Patrick Massot (Feb 09 2021 at 09:39):

The other extreme reserving AI to neural network (or even machine learning) is also ridiculous.

view this post on Zulip Andrew Ashworth (Feb 09 2021 at 09:48):

I feel like AI can be used to describe any algorithm that is used to replace what traditionally would be human decision-making or attempts to emulate an intelligent decision-maker. Which is why Deep Blue is an AI despite being a bunch of computers stapled to graph search algorithms and nobody snickers when we talk about video game AI despite most of them being very simple state machines

view this post on Zulip Mario Carneiro (Feb 09 2021 at 09:51):

AI is any algorithm you don't understand yet

view this post on Zulip Kevin Buzzard (Feb 09 2021 at 09:52):

so then simp is definitely an AI :D (as is type class inference)

view this post on Zulip Andrew Ashworth (Feb 09 2021 at 09:54):

I'm not sure if it is right now, but it definitely would be once we give simp a nice animated paper clip avatar that pops up in the goal window when it produces squeeze simp results

view this post on Zulip Johan Commelin (Feb 09 2021 at 10:13):

For all linux users out there: this is an oblique reference to another microsoft product...

view this post on Zulip Patrick Massot (Feb 09 2021 at 10:49):

Jasmin Blanchette said:

Just like you guys distinguish between elementary math and advanced math, we have non-AI vs. AI. It can't be defined, but if there's not a substantial heuristic / ad hoc component, it's not an AI.

Kevin, note that refl seems to fit the bill pretty well.

view this post on Zulip Kevin Buzzard (Feb 09 2021 at 11:07):

refl is an AI because I don't understand it. For example the I've never managed to figure out why the description in the reference manual implies that quot.lift f h (quot.mk r a) = f a can be proved by rfl.


Last updated: May 11 2021 at 21:10 UTC