9 ms·

Kurt Gödel's Letter to John von Neumann (1956) [pdf]

183 points by headalgorithm 8y ago

bradleyjg 8y ago
Apparently the young man didn’t go into medicine after all: https://en.m.wikipedia.org/wiki/Richard_M._Friedberg https://en.m.wikipedia.org/wiki/Richard_M._Friedberg
- defertoreptar 8y ago
  Here's a 1958 article that suggests he made it to at least his second year in medical school. https://www.thecrimson.com/article/1958/1/7/friedberg-finds-computer-shows-ability-to/ https://www.thecrimson.com/article/1958/1/7/friedberg-finds-... Interesting tidbit: > "If we are ever to make a machine that will speak, understand or translate human language, solve mathematical problems with imagination, practice a profession or direct an organization, either we must reduce these activities to a science so exact that we can tell a machine precisely how to go about doing them or we must develop a machine that can do things without being told precisely how,"
  - lioeters 8y ago
    It always amazes me how far-seeing some people were in the early (and pre-) history of computers. The quote above shows such insight/intuition into the future potential of machines, the need for program correctness, the role and nature of machine learning.
segfaultbuserr 8y ago
Could someone adds the historical background of Godel's question?
- earthicus 8y ago
  These letters contain some of the first discussions of computational complexity theory, and von Neumann immediately identifies P vs NP as a central problem in the field. The work was unpublished and undeveloped, as von Neumann became ill and died around this time. Edit: I double-checked my biography of von Neumann and in fact, as the poster below indicated, his responses (if he was able to make any) aren't available. This letter of Goedel has identified an NP problem, and he's asking if it can be solved in polynomial time, so we can't credit von Neumann for identifiying the problem with certainty.
  - lqet 8y ago
    A common phrase you often hear when people try to explain the impressive technological leaps made in the 20th century is "war is the father of all things", meaning of course that WWII was a major catalyst for technological advancement. I always wondered if it shouldn't be phrased as "John von Neumann is the father of all things."
    - SquishyPanda23 8y ago
      I'dd add Poincaré. John von Neumann and Henri Poincaré certainly deserve credit for a shocking amount of modern advancement in math and science.
  - shmageggy 8y ago
    > von Neumann immediately identifies P vs NP as a central problem in the field. Do you have a source for this? I'd love to read von Neumann's reply. All I found from a search is this stackexchange answer stating that there is no known reply. https://cstheory.stackexchange.com/questions/41209/did-von-neumann-answer-to-g%C3%B6dels-letter https://cstheory.stackexchange.com/questions/41209/did-von-n...
    - earthicus 8y ago
      My source for learning about the exchange was a biography of von Neumann by Macrae, but i double-checked it and it appears you are correct. I was mis-remembering how much of the correspondence von Neumann was able to contribute at that point. I've corrected my original comment accordingly, thank you.
- jandrese 8y ago
  It looks like he's asking about the halting problem. I'm not a mathematician, but it looks like he's asking if a machine could be built that could solve all of mathematics in linear or quadratic time.
  - kkylin 8y ago
    No, not quite. Roughly speaking, he's asking about the computational complexity of solving problems (producing proofs of statements in first-order predicate logic) with a given bound N on the size of the solution. This is computable becaue the number of solutions (i.e., proofs) of length <= N is finite, and one can in principle just enumerate them all and check. Goedel's question is how the running time of producing a solution of size <= N (or finding that there is no solution of size <= N) grows with N, with the thinking that if no proof of a reasonable size can be found, one might as well not bother looking anymore.
RobertoG 8y ago
Well, being the guy to who Kurt Gödel ask mathematical advice has to be a curious position to be.
- wycs 8y ago
  Well, Von Neumann was likely the smartest man who ever lived.
  - goatlover 8y ago
    There's a few other candidates for that title, and not just in the 20th century.
    - nabla9 8y ago
      Many of the other candidates of that time agreed that Von Neumann was the smartest among them. He had a mind like a racecar. Quoting Eugene Wigner: > "I have known a great many intelligent people in my life. I knew Planck, von Laue and Heisenberg. Paul Dirac was my brother in law; Leo Szilard and Edward Teller have been among my closest friends; and Albert Einstein was a good friend, too. But none of them had a mind as quick and acute as Jansci [John] von Neumann. I have often remarked this in the presence of those men and no one ever disputed. > But Einstein's understanding was deeper even than von Neumann's. His mind was both more penetrating and more original than von Neumann's. And that is a very remarkable statement. Einstein took an extraordinary pleasure in invention. Two of his greatest inventions are the Special and General Theories of Relativity; and for all of Jansci's brilliance, he never produced anything as original."
      - defertoreptar 8y ago
        Here's the usual anecdote that goes along with von Neumann threads: > The following problem can be solved the easy way or the hard way: > "Two trains 200 miles apart are moving toward each other; each one is going at a speed of 50 miles per hour. A fly starting on the front of one of the trains flies back and forth between them at a rate of 75 miles per hour. It does this until the trains collide and crush the fly to death. What is the total distance the fly has flown?" > In a strict mathematical sense the fly actually hits each train an infinite number of times before it gets crushed, and one could solve the problem the hard way with pencil and paper by summing an infinite series of distances. This is the way that most trained mathematicians will solve the problem. Conversely a mathematical novice will most likely solve the problem the easy way - since the trains are 200 miles apart and each train is going 50 miles an hour, it takes 2 hours for the trains to collide, therefore the fly was flying for two hours, at a rate of 75 miles per hour, and so the fly must have flown 150 miles. Easy. > When this problem was posed to John von Neumann, he immediately replied, "150 miles." > "Ah, I see you've heard this one before, Professor von Neumann. Nearly everyone tries to sum the infinite series." "What do you mean?" asked von Neumann. "That's how I did it!"
TaupeRanger 8y ago
The story of Von Neumann's death is actually quite interesting. The government kept a guard by his death bed to be sure he didn't divulge any state secrets while on mind numbing pain medications. It is well documented that, after Von Neumann learned of his terminal pancreatic cancer, he became horrified of death and would cry out at night, even resorting to last-minute conversations with a priest on his deathbed (though he was an atheist throughout his life). His mother died during his illness and his family tried to hide it from him. But he eventually figured it out and took a turn for the worst. It's all very sad in the same way it would be for anyone, but in Von Neumann's case it makes one wonder what else he would've accomplished in the next two or three decades of life.
- defertoreptar 8y ago
  I've always wondered. What kind of government secrets were they worried he'd let slip? It's been so long that they must be declassified by now. His breadth of expertise was so great, it'd be interesting to know what kind of contributions he was making to the government.
  - nwah1 8y ago
    Could file a FOIA and find out.
    - btrettel 8y ago
      A list of his work with the Atomic Energy Commission could be obtained from OSTI: https://www.osti.gov/freedom-information-act-foia https://www.osti.gov/freedom-information-act-foia For the Department of Defense, you could get a list from DTIC: https://discover.dtic.mil/email-form-dtic-foia https://discover.dtic.mil/email-form-dtic-foia I doubt much if anything interesting by von Neumann is still classified or limited. If something is still classified it's probably because no one wanted to declassify it, not that it's sensitive. If anyone does file FOIA requests for these lists, contact me, as I'm interested but not interested enough to file the requests. See my HN profile for a link to my personal website with a contact form.
ldenoue 8y ago
Mobile version here https://docushow.com/viewdocchris?url=http%3A//www.cs.cmu.edu/%7Eaada/courses/15251s15/www/notes/godel-letter.pdf&dev=2 https://docushow.com/viewdocchris?url=http%3A//www.cs.cmu.ed...
lordnacho 8y ago
Gödel must have understood von Neumann to have been very very interested in his work? I mean of course he was, but to the degree that even if he were ill he'd be thinking about math. Otherwise it reads like "hey, hope you get better, now do you think P == NP?"
- gumby 8y ago
  > "hey, hope you get better, now do you think P == NP?" That was my read of it and I found it heartening. Having had a near-fatal illness myself I was bummed at the time by all the moaning about it. People were really talking about their issues, not mine (OK, kid freaking out about becoming an orphan was something for me to address). My own head was still full of stuff I wanted to do in the future (and what to do about my own therapeutic plan) and I would have been delighted to talk to someone who would think that way too. The great thing about the net is I could (textually) talk to friends far away who had no idea I was sick.
  - djmips 8y ago
    Isn't your death more about the people left behind? I mean you're not going to have any problems once you're dead.
- triska 8y ago
  Without context, one could indeed get this impression. However, Kurt Gödel and John von Neumann had met each other and exchanged letters long before that already, and Gödel was fully aware that von Neumann was interested in this area. For example, quoting from: https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_theorems https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_... “Gödel announced his first incompleteness theorem at a roundtable discussion session on the third day of the conference. The announcement drew little attention apart from that of von Neumann, who pulled Gödel aside for conversation. Later that year, working independently with knowledge of the first incompleteness theorem, von Neumann obtained a proof of the second incompleteness theorem, which he announced to Gödel in a letter dated November 20, 1930 (Dawson 1996, p. 70).” To that letter, Gödel politely replied that he had already submitted the result for publication.
earthicus 8y ago
Here's a nice article that discusses the historical importance of the letter and the problem Goedel raises: https://ecommons.cornell.edu/bitstream/handle/1813/6910/89-994.pdf?sequence=1 https://ecommons.cornell.edu/bitstream/handle/1813/6910/89-9...
pimmen 8y ago
John von Neumann seems like the man you would certainly want to meet. Apparently, he was good at talking to children and treating them with respect, same thing with people who weren't up to his abilities (which, let's be fair, is basically everyone) so he would probably not be condescending towards you. He had a great sense of humor and loved telling jokes, and he probably had a story or two about when he drove into someone else. He came from a wealthy, cultural family in Hungary, was fluent in Greek and Latin and was always well dressed so he could probably offer very deep discussions outside science too. And, he was one of the first contributors to computer science and thus could probably offer a great discussion to us techies. His war stories are actual war stories. If I could meet some historical person for an interview, von Neumann is at the top of the list.
gonzus 8y ago
I have always wanted to get my hands on the "definitive" book about von Neumann, whom I find a fascinating character. Is there such a thing? Any recommendations?
- Upvoter33 8y ago
  The Martian's Daughter. A Memoir not definitive but an interesting read from his daughter, quite an accomplished person in her own right.
- HNLurker2 8y ago
  I would recommend these videos. A German documentary with subtitles and this: https://youtu.be/97hfRcrYBtE https://youtu.be/97hfRcrYBtE https://youtu.be/Y2jiQXI6nrE https://youtu.be/Y2jiQXI6nrE
- adharmad 8y ago
  Martians of Science: Five Physicists Who Changed the Twentieth Century - Istvan Hargittai
- loganv 8y ago
  While probably not "definitive" or even specifically about von Neumann, Turing's Cathedral by George Dyson had a lot of info about him and follows his work in computing, physics, and mathematics over the course of his career.
ot 8y ago
A few comments imply that this introduces the question of P ?= NP, and while it indeed is defining a complexity problem, this is about satisfiability of first order predicates logic, that is formulas with sets and quantifiers, while SAT is about propositional logic. First order logic was famously proved incomputable by Godel himself, so here he's asking whether we can bound the number of steps given the size of the proof, not the size of the input (formula length), which is the way complexity is usually defined. In practice, he's saying that tractable theorems must have reasonably sized proofs (to be understood by a human), and there might be an algorithm that is efficient enough in finding short proofs.
- earthicus 8y ago
  According to [1], the question Goedel raises is equivalent to P vs NP, although clearly not phrased in the same language. The author claimes Goedel's phi(n) is polynomially bounded if and only if P=NP. Do you disagree with that statement? [1] https://ecommons.cornell.edu/bitstream/handle/1813/6910/89-994.pdf?sequence=1 https://ecommons.cornell.edu/bitstream/handle/1813/6910/89-9...
  - ot 8y ago
    > The author claimes Goedel's phi(n) is polynomially bounded if and only if P=NP. Do you disagree with that statement? It would be trivially true if Godel was talking about propositional logic (proof size is polinomially bounded by definition of NP). I don't know if that's true for first order logic (it's not as obvious to me as the author seems to imply) but even in that case it would be a non-trivial connection, so I believe it's a stretch to say that this was about P and NP.
- deleted 8y ago
  [deleted]
neokantian 8y ago
If you look at the Isabelle (https://isabelle.in.tum.de/overview.html https://isabelle.in.tum.de/overview.html) and Coq (https://coq.inria.fr https://coq.inria.fr) proof assistants, you can see that enumerating all possible expressions F and automatically verify if there is a proof of length less than n, has not turned out to be a fruitful approach. These tools do not even particularly try to do that ... ;-)

183 points by headalgorithm 8y ago

Apparently the young man didn’t go into medicine after all: https://en.m.wikipedia.org/wiki/Richard_M._Friedberg https://en.m.wikipedia.org/wiki/Richard_M._Friedberg

defertoreptar 8y ago
Here's a 1958 article that suggests he made it to at least his second year in medical school. https://www.thecrimson.com/article/1958/1/7/friedberg-finds-computer-shows-ability-to/ https://www.thecrimson.com/article/1958/1/7/friedberg-finds-... Interesting tidbit: > "If we are ever to make a machine that will speak, understand or translate human language, solve mathematical problems with imagination, practice a profession or direct an organization, either we must reduce these activities to a science so exact that we can tell a machine precisely how to go about doing them or we must develop a machine that can do things without being told precisely how,"
- lioeters 8y ago
  It always amazes me how far-seeing some people were in the early (and pre-) history of computers. The quote above shows such insight/intuition into the future potential of machines, the need for program correctness, the role and nature of machine learning.

segfaultbuserr 8y ago

Could someone adds the historical background of Godel's question?

earthicus 8y ago
These letters contain some of the first discussions of computational complexity theory, and von Neumann immediately identifies P vs NP as a central problem in the field. The work was unpublished and undeveloped, as von Neumann became ill and died around this time. Edit: I double-checked my biography of von Neumann and in fact, as the poster below indicated, his responses (if he was able to make any) aren't available. This letter of Goedel has identified an NP problem, and he's asking if it can be solved in polynomial time, so we can't credit von Neumann for identifiying the problem with certainty.
- lqet 8y ago
  A common phrase you often hear when people try to explain the impressive technological leaps made in the 20th century is "war is the father of all things", meaning of course that WWII was a major catalyst for technological advancement. I always wondered if it shouldn't be phrased as "John von Neumann is the father of all things."
  - SquishyPanda23 8y ago
    I'dd add Poincaré. John von Neumann and Henri Poincaré certainly deserve credit for a shocking amount of modern advancement in math and science.
- shmageggy 8y ago
  > von Neumann immediately identifies P vs NP as a central problem in the field. Do you have a source for this? I'd love to read von Neumann's reply. All I found from a search is this stackexchange answer stating that there is no known reply. https://cstheory.stackexchange.com/questions/41209/did-von-neumann-answer-to-g%C3%B6dels-letter https://cstheory.stackexchange.com/questions/41209/did-von-n...
  - earthicus 8y ago
    My source for learning about the exchange was a biography of von Neumann by Macrae, but i double-checked it and it appears you are correct. I was mis-remembering how much of the correspondence von Neumann was able to contribute at that point. I've corrected my original comment accordingly, thank you.
jandrese 8y ago
It looks like he's asking about the halting problem. I'm not a mathematician, but it looks like he's asking if a machine could be built that could solve all of mathematics in linear or quadratic time.
- kkylin 8y ago
  No, not quite. Roughly speaking, he's asking about the computational complexity of solving problems (producing proofs of statements in first-order predicate logic) with a given bound N on the size of the solution. This is computable becaue the number of solutions (i.e., proofs) of length <= N is finite, and one can in principle just enumerate them all and check. Goedel's question is how the running time of producing a solution of size <= N (or finding that there is no solution of size <= N) grows with N, with the thinking that if no proof of a reasonable size can be found, one might as well not bother looking anymore.

RobertoG 8y ago

Well, being the guy to who Kurt Gödel ask mathematical advice has to be a curious position to be.

wycs 8y ago
Well, Von Neumann was likely the smartest man who ever lived.
- goatlover 8y ago
  There's a few other candidates for that title, and not just in the 20th century.
  - nabla9 8y ago
    Many of the other candidates of that time agreed that Von Neumann was the smartest among them. He had a mind like a racecar. Quoting Eugene Wigner: > "I have known a great many intelligent people in my life. I knew Planck, von Laue and Heisenberg. Paul Dirac was my brother in law; Leo Szilard and Edward Teller have been among my closest friends; and Albert Einstein was a good friend, too. But none of them had a mind as quick and acute as Jansci [John] von Neumann. I have often remarked this in the presence of those men and no one ever disputed. > But Einstein's understanding was deeper even than von Neumann's. His mind was both more penetrating and more original than von Neumann's. And that is a very remarkable statement. Einstein took an extraordinary pleasure in invention. Two of his greatest inventions are the Special and General Theories of Relativity; and for all of Jansci's brilliance, he never produced anything as original."
    - defertoreptar 8y ago
      Here's the usual anecdote that goes along with von Neumann threads: > The following problem can be solved the easy way or the hard way: > "Two trains 200 miles apart are moving toward each other; each one is going at a speed of 50 miles per hour. A fly starting on the front of one of the trains flies back and forth between them at a rate of 75 miles per hour. It does this until the trains collide and crush the fly to death. What is the total distance the fly has flown?" > In a strict mathematical sense the fly actually hits each train an infinite number of times before it gets crushed, and one could solve the problem the hard way with pencil and paper by summing an infinite series of distances. This is the way that most trained mathematicians will solve the problem. Conversely a mathematical novice will most likely solve the problem the easy way - since the trains are 200 miles apart and each train is going 50 miles an hour, it takes 2 hours for the trains to collide, therefore the fly was flying for two hours, at a rate of 75 miles per hour, and so the fly must have flown 150 miles. Easy. > When this problem was posed to John von Neumann, he immediately replied, "150 miles." > "Ah, I see you've heard this one before, Professor von Neumann. Nearly everyone tries to sum the infinite series." "What do you mean?" asked von Neumann. "That's how I did it!"

TaupeRanger 8y ago

The story of Von Neumann's death is actually quite interesting. The government kept a guard by his death bed to be sure he didn't divulge any state secrets while on mind numbing pain medications. It is well documented that, after Von Neumann learned of his terminal pancreatic cancer, he became horrified of death and would cry out at night, even resorting to last-minute conversations with a priest on his deathbed (though he was an atheist throughout his life). His mother died during his illness and his family tried to hide it from him. But he eventually figured it out and took a turn for the worst. It's all very sad in the same way it would be for anyone, but in Von Neumann's case it makes one wonder what else he would've accomplished in the next two or three decades of life.

defertoreptar 8y ago
I've always wondered. What kind of government secrets were they worried he'd let slip? It's been so long that they must be declassified by now. His breadth of expertise was so great, it'd be interesting to know what kind of contributions he was making to the government.
- nwah1 8y ago
  Could file a FOIA and find out.
  - btrettel 8y ago
    A list of his work with the Atomic Energy Commission could be obtained from OSTI: https://www.osti.gov/freedom-information-act-foia https://www.osti.gov/freedom-information-act-foia For the Department of Defense, you could get a list from DTIC: https://discover.dtic.mil/email-form-dtic-foia https://discover.dtic.mil/email-form-dtic-foia I doubt much if anything interesting by von Neumann is still classified or limited. If something is still classified it's probably because no one wanted to declassify it, not that it's sensitive. If anyone does file FOIA requests for these lists, contact me, as I'm interested but not interested enough to file the requests. See my HN profile for a link to my personal website with a contact form.

ldenoue 8y ago

Mobile version here https://docushow.com/viewdocchris?url=http%3A//www.cs.cmu.edu/%7Eaada/courses/15251s15/www/notes/godel-letter.pdf&dev=2 https://docushow.com/viewdocchris?url=http%3A//www.cs.cmu.ed...

lordnacho 8y ago

Gödel must have understood von Neumann to have been very very interested in his work? I mean of course he was, but to the degree that even if he were ill he'd be thinking about math. Otherwise it reads like "hey, hope you get better, now do you think P == NP?"

gumby 8y ago
> "hey, hope you get better, now do you think P == NP?" That was my read of it and I found it heartening. Having had a near-fatal illness myself I was bummed at the time by all the moaning about it. People were really talking about their issues, not mine (OK, kid freaking out about becoming an orphan was something for me to address). My own head was still full of stuff I wanted to do in the future (and what to do about my own therapeutic plan) and I would have been delighted to talk to someone who would think that way too. The great thing about the net is I could (textually) talk to friends far away who had no idea I was sick.
- djmips 8y ago
  Isn't your death more about the people left behind? I mean you're not going to have any problems once you're dead.
triska 8y ago
Without context, one could indeed get this impression. However, Kurt Gödel and John von Neumann had met each other and exchanged letters long before that already, and Gödel was fully aware that von Neumann was interested in this area. For example, quoting from: https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_theorems https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_... “Gödel announced his first incompleteness theorem at a roundtable discussion session on the third day of the conference. The announcement drew little attention apart from that of von Neumann, who pulled Gödel aside for conversation. Later that year, working independently with knowledge of the first incompleteness theorem, von Neumann obtained a proof of the second incompleteness theorem, which he announced to Gödel in a letter dated November 20, 1930 (Dawson 1996, p. 70).” To that letter, Gödel politely replied that he had already submitted the result for publication.

earthicus 8y ago

Here's a nice article that discusses the historical importance of the letter and the problem Goedel raises: https://ecommons.cornell.edu/bitstream/handle/1813/6910/89-994.pdf?sequence=1 https://ecommons.cornell.edu/bitstream/handle/1813/6910/89-9...

pimmen 8y ago

John von Neumann seems like the man you would certainly want to meet. Apparently, he was good at talking to children and treating them with respect, same thing with people who weren't up to his abilities (which, let's be fair, is basically everyone) so he would probably not be condescending towards you. He had a great sense of humor and loved telling jokes, and he probably had a story or two about when he drove into someone else. He came from a wealthy, cultural family in Hungary, was fluent in Greek and Latin and was always well dressed so he could probably offer very deep discussions outside science too. And, he was one of the first contributors to computer science and thus could probably offer a great discussion to us techies. His war stories are actual war stories. If I could meet some historical person for an interview, von Neumann is at the top of the list.

gonzus 8y ago

I have always wanted to get my hands on the "definitive" book about von Neumann, whom I find a fascinating character. Is there such a thing? Any recommendations?

Upvoter33 8y ago
The Martian's Daughter. A Memoir not definitive but an interesting read from his daughter, quite an accomplished person in her own right.
HNLurker2 8y ago
I would recommend these videos. A German documentary with subtitles and this: https://youtu.be/97hfRcrYBtE https://youtu.be/97hfRcrYBtE https://youtu.be/Y2jiQXI6nrE https://youtu.be/Y2jiQXI6nrE
adharmad 8y ago
Martians of Science: Five Physicists Who Changed the Twentieth Century - Istvan Hargittai
loganv 8y ago
While probably not "definitive" or even specifically about von Neumann, Turing's Cathedral by George Dyson had a lot of info about him and follows his work in computing, physics, and mathematics over the course of his career.

ot 8y ago

A few comments imply that this introduces the question of P ?= NP, and while it indeed is defining a complexity problem, this is about satisfiability of first order predicates logic, that is formulas with sets and quantifiers, while SAT is about propositional logic. First order logic was famously proved incomputable by Godel himself, so here he's asking whether we can bound the number of steps given the size of the proof, not the size of the input (formula length), which is the way complexity is usually defined. In practice, he's saying that tractable theorems must have reasonably sized proofs (to be understood by a human), and there might be an algorithm that is efficient enough in finding short proofs.

earthicus 8y ago
According to [1], the question Goedel raises is equivalent to P vs NP, although clearly not phrased in the same language. The author claimes Goedel's phi(n) is polynomially bounded if and only if P=NP. Do you disagree with that statement? [1] https://ecommons.cornell.edu/bitstream/handle/1813/6910/89-994.pdf?sequence=1 https://ecommons.cornell.edu/bitstream/handle/1813/6910/89-9...
- ot 8y ago
  > The author claimes Goedel's phi(n) is polynomially bounded if and only if P=NP. Do you disagree with that statement? It would be trivially true if Godel was talking about propositional logic (proof size is polinomially bounded by definition of NP). I don't know if that's true for first order logic (it's not as obvious to me as the author seems to imply) but even in that case it would be a non-trivial connection, so I believe it's a stretch to say that this was about P and NP.
deleted 8y ago
[deleted]

neokantian 8y ago

If you look at the Isabelle (https://isabelle.in.tum.de/overview.html https://isabelle.in.tum.de/overview.html) and Coq (https://coq.inria.fr https://coq.inria.fr) proof assistants, you can see that enumerating all possible expressions F and automatically verify if there is a proof of length less than n, has not turned out to be a fruitful approach. These tools do not even particularly try to do that ... ;-)