@jcreed

484 Followers
212 Following
3.9K Posts
theorems, types, tunes, typefaces, terms-of-art, tropes, technicalities. [en/eo, +ε es/zh/fr/pl/jp]
foundationsconstructive, univalent
ghhttps://github.com/jcreedcmu
@kaychaks Yes! the Lean FRO team already spans several countries, and remote work from anywhere is definitely in scope for this job posting.
@aparrish @chrisamaphone oh yeah yeah word for sure I hear you I've been on that meta-vacillation lately, you know? alternating between decisive and indecisive? Like... 5:00am I don't know ANYTHING bruh and then 5:01am I've got the self-assurance of a baby who just said dada for the first time and 5:02am I'm in an infinite hem/haw loop again
@mirabilos The company the (fully remote) jobs are actually for is the Lean Focused Research Organization https://lean-lang.org/fro/about/ which I believe is based in the US, if that's the information you're interested in!
Lean Programming Language

Lean is a theorem prover and programming language that enables correct, maintainable, and formally verified code.

Lean Language

@mirabilos You might enjoy this relevant episode of the trivia quiz show "Lateral" https://www.youtube.com/watch?v=iyt6cunJ8qc

(different country, same idea :)

Anguilla's surprise windfall

YouTube
@mirabilos I think the fact that the site that manages the job listings https://en.wikipedia.org/wiki/Lever_(company) has a .co domain is unrelated to their place of business. They look like they're based in SF.
Lever (company) - Wikipedia

Vibe coding is writing horrible un-maintainable code with an AI. I propose “gremlin coding” for when you’re writing horrible un-maintainable code all yourself on purpose
If 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

Lean Programming Language

Lean is a theorem prover and programming language that enables correct, maintainable, and formally verified code.

Lean Language
- 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
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
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