Our great sponsors

I'm not sure how useful this will be, since the question asks for a simple program, but maybe the LEAN theorem prover can be used to type in theorem statements. The theorems can be categorised by placing different theorems in different files (say one for algebra, another for analysis, and so on). Searching for specific theorems can be done by searching ("grepping", in Linux lingo) for the relevant text in the folder containing all the files.
NOTE:
The number of mentions on this list indicates mentions on common posts plus user suggested alternatives.
Hence, a higher number means a more popular project.
Related posts
 There’s more to mathematics than rigour and proofs
 The Lean Theorem Prover
 Is there a formal proof that all integers can be expressed as the sum of four squares?
 Why is simplicity so unreasonably effective at scientific explanation?
 This is just an attempt I'm trying to get better at writing proofs I know I'm an idiot so please be constructive if you are criticizing