Can we use the classical math proof as guideline

39 views

Skip to first unread message

Filip Cernatescu

unread,

Nov 6, 2019, 2:05:55 AM11/6/19

to Metamath

Can we use classical math proof as guideline for proving formal metamath theorems or formal proofs are totaly different?

Alexander van der Vekens

unread,

Nov 6, 2019, 3:08:26 AM11/6/19

to Metamath

Hi Filip,

of course you can - I used classical proofs as guideline for my proofs of the friendship theorem (see Huneke's paper) and cramer's rule (see Wikipedia!). But it's only a "guideline" - there is (usually) much more work to do, searching for theorems or proving them to fill the gaps within the classical proofs.