These projects exist, and are so easy that we don't even bother to use AI on them. As an example of high-level reasoning, Metamath has a body of theorems of ZFC

These projects exist, and are so easy that we don't even bother to use AI on them. As an example of high-level reasoning, Metamath has a body of theorems of ZFC using classical logic [0]. This body of theorems is written out using entirely formal (symbolic, syntactic) reasoning. Over 32,000 theorems are checked in total, at a rate of around 6 kilotheorems per second. If we recall that proof search is (Turing-)undecidable, for the systems that we care about, then it becomes unsurprising that we do not put AI to the task, other than as a light at the end of the tunnel, since proof search is not only AI-hard, but as impossible for AIs as for humans. That said, there have been constant improvements to the automated generation of human-readable proofs, and the papers have the same shape as AI research papers from previous generations of AI, with expert systems and inference engines [2][3]. Your focus on IQ tests is a little unhealthy [1]. [0] http://us.metamath.org/mpeuni/mmset.html http://us.metamath.org/mpeuni/mmset.html [1] https://en.wikipedia.org/wiki/Intelligence_quotient#History https://en.wikipedia.org/wiki/Intelligence_quotient#History [2] https://www.ijcai.org/Proceedings/15/Papers/172.pdf https://www.ijcai.org/Proceedings/15/Papers/172.pdf [3] http://poincare.matf.bg.ac.rs/~janicic/papers/2014-amai-aftarski.pdf http://poincare.matf.bg.ac.rs/~janicic/papers/2014-amai-afta...