I would like to see computational assistance for formalizing existing mathematical results. The goal would be a system that could take a paper and output its proofs in formalized form. Ultimately, this would enable us to vet all published mathematical results and deliver them as formal proofs, which could then be used as training inputs for future proof systems.