Comment by ogogmad
"Architect of computer intelligence" - I'm sure Church was an accomplished logician, but his contribution to "computer intelligence", which I imagine is supposed to mean AI/ML, is absolutely nil.
On a separate note, I don't think lambda calculus is really maths. It's more like clever notation. The merits of any notation are subjective. It's interesting how Church never cared about how that particular idea of his inspired the design of certain programming languages - which are ultimately notations, and therefore subjective in their merits.
"Lambda calculus" is sometimes used to mean "simply typed lambda calculus", which is mainly used to refer to simple type theory (STT), which is also called "Church's type theory". STT is also often identified with higher-order logic, since just two primitive types (basic "entities" like chairs and the "truth values" T/F) and the function type (a --> b) suffice to express arbitrary logical objects. STT is indeed an invention of Church, and it has had a major influence on other modern type theories, which are often described as extensions of simple type theory. These also influenced some programming languages with complex type system, like Haskell.