If you download this Lean project onto your own computer using leanproject
by typing leanproject get ImperialCollegeLondon/Lean-UROP (or whatever
I end up calling it on GitHub),
you will just be able to edit it and experiment with it. It's lots of half-written Lean projects, some big, some small, all in their own directories.