In the theory of formal languages, Conway's problem asks, if the greatest solution $X$ of $LX = XL$, for some finite language $L$, is regular. Now, we know that this does not hashave to be the case, but it was an open problem for many years.
It goes back to his book Regular algebra and finite machines, which grew out of the work of one of his PhD students. In the book, he gave a proof of Parikh's theorem that is quite short and elegant. His student published the proof. The original proof is very long and technical.
I studied mathematics, and did some group theory classes. So surely I knew about John Conway. As I started my PhD in theoretical computer science, it was a little bit surprising to find out that he had done some work in formal language theory. The book has a somewhat unconventional take on it. As far as I remember, in it he introduced biregular relations, which seemed to be quite similar to what was later introduceintroduced as an algebraic treatment of transductions. Also, he introduced the factor matrix of some regular language, which is also called the universal automaton.