1. 18

People might know proof assistants such as Coq or Isabelle/HOL, but the field of automatic proving has been active since around 1960 and is interesting on its own. This prover, written in C and free (GPL), has done very well in the main prover competition for first-order logic. It’s also a very nice C codebase.

See the wikipedia page for a short summary, and this paper for more details on the theory and implementation.