Are there any lessons or tricks here that we can apply to software engineering? What kinds of assertions can we express more easily with Lean etc. than with unit tests, fuzz tests, property tests, using our existing testing frameworks?
The main lesson is quite simple: if you can write the test to be uncheatable, ChatGPT can write the code for it.
The main lesson is quite simple: if you can write the test to be uncheatable, ChatGPT can write the code for it.