My Master's thesis is a user-friendly proof assistant. I'm interested in hearing your thoughts and feedback! (The attached link contains a video of my thesis presentation.) https://dev.to/ender_minyard/introducing-starling-a-user-friendly-proof-assistant-1j0

Making proof assistants more user-friendly is definitely a worthy goal to pursue! Something you don't say in your video is who you consider to be your users. You mention both proofs in mathematics and formal verification of software. These are fundamentally the same problem, but the users interested in these two domains have quite different prior experience, so maybe being friendly to one doesn't imply being friendly to the other. Another consideration I see rarely made in this space is that readers of proofs are also a kind of users, even if they never touch the proof assistant themselves.

Super interesting, will have to look further in a two or so weeks! I already have reviewing recent progress in proof assistants on my to-do list.

Great combination; user-friendly and something technical, always interesting to see these types of projects. I have no experience at all in this domain - it seems - if you want to user test on me; feel free. It reminds me a bit of prolog; but no clue if there is any connection.