GusLacerda: I went to a talk by Pfenning on Friday

GusLacerda: and asked him about who here does AR [automated reasoning]

GusLacerda: and the answer was disappointing

GusLacerda: basically, people who are into type theory

aCleverEpithet: yes

GusLacerda: I told him I was interested in "algorithm discovery"

GusLacerda: this was 50% bullshit

GusLacerda: because "algorithm discovery" is a non-existent research area

GusLacerda: but he seemed interested

GusLacerda: I explained the idea... which he and one student seemed to get excited about

aCleverEpithet: it is interesting

GusLacerda: but his conclusion, as far as collaborators go, was: Herb Simon is dead...

[note: to be fair, he did tell me to check out

Raul Valdes-Perez, which is a very good lead. Is this guy actually at CMU?]

aCleverEpithet: hard, but interesting

aCleverEpithet: this is true

GusLacerda: everyone says this

GusLacerda: but that's like saying "AI is hard"

aCleverEpithet: thats a good point actually

GusLacerda: I am happy to make incremental progress

GusLacerda: record people doing it

GusLacerda: figure out how they're doing it

GusLacerda: formalize it

GusLacerda: and implement it

GusLacerda: that's it!

GusLacerda: of course, this only works for reasoning-based tasks

GusLacerda: you can't necessarily figure out what people are doing if it involves unconscious pattern-recognition

aCleverEpithet: yes, i wonder how much that actually comes into play

aCleverEpithet: if it is more or less than we think

GusLacerda: hard to say

GusLacerda: certainly, a lot of the things we find hard to formalize in math, are *not* due to such processes

GusLacerda: but rather due to us not having cognitively-faithful representations

GusLacerda: like diagrammatic reasoning, which we're making progress on

GusLacerda: a lot of math and science is reasoning

aCleverEpithet: definitely

GusLacerda: formalizing it can't be bad

GusLacerda: maybe 100% of algorithm discovery is reasoning

aCleverEpithet: i can't think of any examples of algorithm discovery that are not just reasoning

GusLacerda: me neither

GusLacerda: although in some cases, spatial reasoning is needed

GusLacerda: or maybe that's just mathematical reasoning

aCleverEpithet: yeah, im not usre

aCleverEpithet: i think it's a kind of mathematical reasoning

GusLacerda: well, algorithm discovery IS mathematical discovery

...

GusLacerda: anyway, this stuff is an interesting mix of theoretical and empirical reasoning

[...just like scientific discovery and ordinary mathematical discovery]