Towards a human-style theorem prover for inequalities
Noam Neer

Automatic proving of mathematical theorems is a very difficult
problem. I will focus on a specific domain, namely, (in)equalities in
real numbers, a domain to which many Math Olympiad problems are
dedicated. After a brief introduction to existing approaches for
automatic solution of such problems, I will try to look at solutions
given by humans and see if there are recurring operations that we can
identify and implement efficiently in software.