Yeah my impression is verifying human proof-to-Lean code translation faithfulness is pretty resistant to automation.
Yeah my impression is verifying human proof-to-Lean code translation faithfulness is pretty resistant to automation.