Xujie Si

Proving Olympiad Inequalities by Synergizing LLMs and Symbolic Reasoning