lean4-logic icon indicating copy to clipboard operation
lean4-logic copied to clipboard

Published 20 hours ago • verified publisher icon iehality

Proof of incompleteness theorem via derivability conditions

Open SnO2WMaN opened this issue 1 year ago • 1 comments

SnO2WMaN avatar Nov 20 '23 05:11 SnO2WMaN

HilbertStyleの補題を使っている証明をhttps://github.com/iehality/lean4-logic/blob/master/Logic/AutoProver/Prover.lean のby prover [ ... ]タクティックで置き換えられないだろうか？

iehality avatar Dec 10 '23 13:12 iehality