## Stream: new members

### Topic: Is simp an AI?

#### 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!

#### 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.

#### 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?

#### Johan Commelin (Feb 09 2021 at 08:42):

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

#### Johan Commelin (Feb 09 2021 at 08:43):

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

#### Patrick Massot (Feb 09 2021 at 08:56):

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

#### Eric Wieser (Feb 09 2021 at 08:58):

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

yes

#### Patrick Massot (Feb 09 2021 at 09:00):

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

#### 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!

#### 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

#### Kevin Buzzard (Feb 09 2021 at 09:10):

I call refl an AI.

#### 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.

#### Patrick Massot (Feb 09 2021 at 09:39):

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

#### 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

#### Mario Carneiro (Feb 09 2021 at 09:51):

AI is any algorithm you don't understand yet

#### Kevin Buzzard (Feb 09 2021 at 09:52):

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

#### 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

#### Johan Commelin (Feb 09 2021 at 10:13):

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

#### 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.

#### 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