For A, a common misconception is that models write out lean proofs from the start. They write/develop the Natural Language proofs, and then translate (sometimes not even the same model) to lean afterwards.