Logic Theorist is a program written in 1956 by a team including Herbert Simon, which some people regard as the first AI program (it feels to me like the first proof assistant).