refactor: bring the LeanSAT script into the age of post 2005

[hargoniX]

This PR:

• turns the shell script into a python script
• fixes the unexpected by error. The old code was assuming something of the form := sorry to be replaced with := by tac but now it's substituting inside of a tactic block
• brings the script into the age of multi core CPUs, though care needs to be taken when running with too many jobs as some of this stuff can be quite memory hungry
• uses lake lean so you can actually run it multiple times in a row without cleaning a lake cache (assuming you haven't actually compiled the benchmark files of course)

[github-actions[bot]]

Alive Statistics: 89 / 93 (4 failed)