qrat-lean We are aiming to create a verified QRAT proof checker in Lean; to our knowledge, this would be the first such verified checker. Stay tuned!