unlofl [Promoted Toot]
Amélia Liaothe measure of how many funny symbols a closed curve on the plane draws is its wingding number
| foundations | constructive, univalent |
| gh | https://github.com/jcreedcmu |
@jcreed
- 490 Followers
- 213 Following
- 3.9K Posts
theorems, types, tunes, typefaces, terms-of-art, tropes, technicalities. [en/eo, +ε es/zh/fr/pl/jp]
@hannah Someone also kept putting up a little placard next to a fire extinguisher in a museum stairwell, causing people to stop and study it, and the museum kept taking it down.
Then the museum realized it was selling postcards of a photo of the fire extinguisher with the placard in their gift shop, smuggled in and printed with an existing postcard UPC.
The artist sued for their $10 in royalties. Everyone was very amused and/or pissed off.
edit: its Dove Bradshaw, see reply/thread
I *thought* I had a paper proof of the 1-braid case, but there are some nuances I didn't quite capture, which of course I noticed when I tried to formalize it. A short blogpost rambling about it: https://jcreedcmu.github.io/posts/2025-08-16/
Pepijn
joomy
RobIf this sounds like something you're interested in, feel free to dm or email jason@lean-fro.org or apply through the Lever job posting links above.
- We're delivering "8. Literate Programming & Next‑Generation UX" in the Year 3 roadmap of the FRO:
https://lean-lang.org/fro/roadmap/1900-1-1-the-lean-fro-year-3-roadmap/#8.-literate-programming-&-next%E2%80%91generation-ux
Things that would make for exciting candidates:
- Having frontend experience is great
- Having opinions about what you wish your favorite literate programming system would do is great
- Having opinions about what you wish your favorite proof assistant would do is great
- Interest in being really user-focused is great
- These are full-time positions and we don't have specific plans for internships.
- Both positions are fully remote
- The team's goal is to push forward the state of the art of tooling in the Lean ecosystem, focusing on document authoring, IDE functionality, and web UX.
- We want to expand the set of people that can learn and use Lean, and remove obstacles and annoyances for existing users
- Both positions are fully remote
- The team's goal is to push forward the state of the art of tooling in the Lean ecosystem, focusing on document authoring, IDE functionality, and web UX.
- We want to expand the set of people that can learn and use Lean, and remove obstacles and annoyances for existing users
An update! We have some actual job postings now.
Research Software Engineer (Tooling) https://jobs.lever.co/convergentresearch/b0ef4502-b2a0-4018-9641-33dfeef09820
Senior Research Software Engineer (Tooling)
https://jobs.lever.co/convergentresearch/5a0770d5-b31f-4afa-a434-3b6566d7f867
Research Software Engineer (Tooling) https://jobs.lever.co/convergentresearch/b0ef4502-b2a0-4018-9641-33dfeef09820
Senior Research Software Engineer (Tooling)
https://jobs.lever.co/convergentresearch/5a0770d5-b31f-4afa-a434-3b6566d7f867
Convergent Research - Research Software Engineer (Tooling)
About the Lean Focused Research Organization (FRO) The Lean Focused Research Organization (FRO) is committed to revolutionizing how Lean, a proof assistant and programming language, is utilized across various sectors. We aim to make Lean a cornerstone in formal mathematics, software and hardware verification, software development, AI in mathematics and code synthesis, and new educational methodologies in math and computer science. Our goal is to cultivate a dynamic, decentralized ecosystem that thrives on diversity and collaboration, engages with a global community, and fosters open-source contributions. About the Role We are seeking a talented and motivated Research Software Engineer to join our team at the Lean FRO. As a Research Software Engineer, you will play a crucial role in developing and enhancing Lean, collaborating with leading mathematicians and computer scientists worldwide, and contributing to the FRO’s long-term sustainability and success. You will have the opportuni
Taus