I mean, he obviously was aware of lambda-calculus as a thing that existed (since he used lambda notation for functions!), but might not have bothered to study it very closely. Nowadays the lambda calculus is considered very elegant, but in the 1940s I think it was considered quite weird and not very well known. (I forget who, but I think some famous logician complained that people did not read his thesis because it used the lambda-calculus formalism, or was adviced not to use it for that reason, or something like that.)

I think, actually the main reason it became so popular is exactly because it was implemented in Lisp/Scheme...

Why? Does every compiler writer know all the theoretical underpinnings and generalizations of their work? Or do that make something that solves a problem without investigating the entire universe around it?

From what I understand, he purposefully took ideas from it, but because he did not feel like he understood it fully, he didn’t try to make a full implementation of it.

Don't forget Gödel!