MathRHS: Conclusion Synthesis in the End-to-End Theorem-Proving Pipeline

Many mathematical problems require synthesising a conclusion before a complete theorem statement can be formalised and proved. Evaluations that provide this conclusion in advance skip an important subtask: determining what must be proved. In this study, we investigate where conclusion synthesis should occur in the end-to-end theorem-proving pipeline. We introduce MathRHS, a benchmark of 457 mathematical problems with conclusions (right-hand side) that separates conclusions from problem statements, and compare three settings: standalone conclusion synthesis before autoformalisation, joint synthesis of the conclusion and formal statement, and conclusion synthesis during proving. By evaluating conclusion correctness, formalisation faithfulness, and verified proof success separately, we trace how synthesis performance translates into downstream results. Standalone synthesis substantially improves conclusion accuracy over joint synthesis: from 61.27% to 75.22% for GPT-4.1 and from 45.73% to 82.02% for DeepSeek-V3.2. These improvements also benefit subsequent stages: using DeepSeek-V3.2 for both standalone synthesis and autoformalisation increases faithful autoformalisation from 12.28% to 21.49% and verified proof success from 4.38% to 5.48%. These findings establish conclusion synthesis as an important pipeline design choice: separating it from autoformalisation improves conclusion accuracy and can strengthen downstream prover performance. Nevertheless, the strongest evaluated pipeline proves only 6.36% of problems, highlighting the challenge of integrating correct conclusions through faithful formalisation to verified proofs. We argue that more effort should be put into targeted training for conclusion synthesis to generate more successful end-to-end proofs.