Is `simp` an AI?

Stream: new members

[Huỳnh Trần Khanh]

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!

[Johan Commelin]

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.

[Huỳnh Trần Khanh]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Patrick Massot]

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

[Eric Wieser]

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

[Patrick Massot]

yes

[Patrick Massot]

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

[Kevin Buzzard]

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!

[Eric Wieser]

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

[Kevin Buzzard]

I call refl an AI.

[Jasmin Blanchette]

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.

[Patrick Massot]

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

[Andrew Ashworth]

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

[Mario Carneiro]

AI is any algorithm you don't understand yet

[Kevin Buzzard]

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

[Andrew Ashworth]

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

[Johan Commelin]

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

[Patrick Massot]

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.

[Kevin Buzzard]

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.