Abstract
In the project "Can an AI Get into the University of Tokyo?", we successfully combined a computer algebra system with natural language processing to automatically generate answers to math problems presented in natural language, outperforming humans by far in math at top universities. This was the moment when the real world had caught up with Tarski's proof (1931) that Theory of Real Closed Field is decidable.
Note: This talk will be presented virtually.