2 ms·
Automation of boring theorems for software properties / correctness would be very useful, even if it didn't produce new mathematical results!
by miloignis 5y ago
Automation of boring theorems for software properties / correctness would be very useful, even if it didn't produce new mathematical results!
- qualudeheart 5y agoI would like a thing where I put in a proposition and attempts are made at autocomplete style proofs of the proposition. Maybe you can do that with program synthesis techniques and Lean style theorem provers.