[8note]

This is cool and im not familiar with what lean actually does beyond the words "formal methods"

immediate questions from reading:

* what is rfl?

* what is decide?

i spent a lot of time looking for where these keywords(? declarations?) were made and i still dont know what they end up meaning

[derdi]

These are both "tactics". The article defines tactics as "instructions that help reduce the current goal". Writing a proof consists of starting with the thing to be proved and then writing a sequence of tactics to break the problem up into progressively easier and easier problems, until everything is broken down into things that are trivially true.

"rfl" stands for "reflexivity", the mathy term for "everything is equal to itself". As the article says, "[rfl] deems two things equal if they are equal by computation". That is to say, if the current subproblem is of the form "prove x = y" where both x and y are some sort of expressions that clearly evaluate to the same value, then applying rfl will finish the proof and mark this problem as solved.

"decide" is another tactic. Not sure where you got it from, I don't see it mentioned in this article. But basically it's a more powerful "I don't want to write out all the steps of this, please try to prove it for me" command.