LLM assistant for Lean

Stream: Machine Learning for Theorem Proving

[Mario Xerxes Castelán Castro 🇲🇽]

Kim Morrison ha dicho:

GasStationManager, I have a preliminary implementation of dyadic rationals at lean#9993. If you'd like to take a look at that and push proofs for any of the sorries that would be lovely! (Or anyone else, of course. I've just spun up a claude session that is working on it, but I have low expectations that it will make any progress without close supervision.)

What setup do you use for using Claude with Lean?