matt-w-horn
- 10 skills
- 0 followers
- 1 day ago last updated
- ▌ Life Paths · matt-w-horn bundleStructured process for mapping realistic long-term life and career paths for a person, grounded in their actual record and finances rather than generic advice. Use this whenever someone asks for help figuring out what to do with their life or career, wants a long-term or phased plan, mentions retirement or FIRE timing alongside career choices, asks whether they could realistically become or achieve something, wants purpose or direction, is at a crossroads (job offer, layoff, burnout, sabbatical, windfall, relocation), or asks to compare possible futures. Trigger even when they ask only a piece of it, like "review my retirement model and tell me when I can quit," "should I take this offer or go independent," or "what am I actually good at" - the pieces connect, and this skill covers the whole.
- ▌ Writing Axes · matt-w-horn bundleAudience-and-goal-first drafting, review, and rewriting for any human-facing prose. Use whenever the user asks to write, rewrite, draft, critique, review, or edit a document, including blog posts, READMEs, papers, emails, docs, runbooks, error messages, release notes, incident reports, announcements, and forum posts. Also use when asked for a title, headline, or subject line, or to check something before posting or publishing it to a public venue; when asked to "de-AI", "de-slop", "strip AI tells", or "make this sound like me"; when asked why text sounds like AI, cringe, amateurish, or unconvincing; when asked to "make this readable", to write for non-native readers, or for docs that translate well, including Simplified Technical English, STE, and ASD-STE100; when asked who a piece is for, or whether a document is worth writing at all. Also use before drafting anything longer than a few paragraphs, even when the request is just "write X".
- ▌ Financial Planning · matt-w-horn bundleBuild a grounded, verified long-horizon financial plan for a person - accumulation, financial-independence timing, drawdown, and the decision rules to run it by. Use this whenever someone asks when they can retire or go work-optional, wants a FIRE or retirement plan built or reviewed, brings a spreadsheet or planner document to audit, asks about safe withdrawal rates, savings schedules, drawdown strategy, or whether their money supports a life change (quitting, sabbatical, going independent, relocating). Trigger even for partial asks like "check my retirement math" or "how much do I need to leave my job" - the pieces need the whole model. Pairs with the life-paths skill (this skill prices a chosen life; that one chooses it), but runs fully standalone.
- ▌ Lake · matt-w-hornBuild, configure, and troubleshoot Lean 4 projects with Lake, Lean's build tool and package manager. Use whenever a Lean build, toolchain, or editor setup is involved — `lake build` fails, hangs, or starts recompiling Mathlib from source; the Mathlib cache will not download; a project needs setting up from scratch; dependencies or `lake-manifest.json` need updating; `lean-toolchain` needs changing; errors appear deep inside Mathlib after bumping its revision, which almost always means a version mismatch rather than a real error; or a Lean project will not load in the editor and the language server hangs or spins. Also use for elan toolchain management, trimming imports, and "how do I start a Lean project with Mathlib".
- ▌ Loogle · matt-w-hornSearch Lean 4 and Mathlib for an existing lemma or definition by name, by subexpression shape, or by what the statement concludes. Use whenever working on a Lean proof and about to prove something from scratch, guess a Mathlib lemma name from memory, or ask "is there already a lemma for this?" — loogle answers in seconds where grepping Mathlib source or guessing names takes minutes and often fails. Works against any local Lean/Lake project whose toolchain matches loogle's build, and there is a hosted instance needing no install at all.
- ▌
- ▌
- ▌ Lean Refactoring · matt-w-horn bundleSimplify, golf, shorten, deduplicate, or restructure existing Lean 4 proofs without changing what is proved. Use for simplification and cleanup passes, "make this proof shorter", reducing line count, collapsing tactic blocks, converting tactic proofs to term proofs, and merging duplicated proof work — and for the guard question every such pass owes an answer, "did this refactor change any statement?". The contract is that statements stay frozen while proof bodies change freely. For writing a new proof, fixing a broken one, or designing a statement, use lean-proving instead.
- ▌ Lean Verification · matt-w-horn bundleCheck whether Lean work actually establishes what it claims. Use whenever the question is "does this really prove X?", "does this build?", "is this sorry-free?", "is my theorem vacuous or junk-true?", "does anything actually satisfy these hypotheses?", "has anyone already formalized this?", or "does this meet my acceptance criteria" — and whenever working through a list of release requirements, auditing a library before tagging it, or reviewing a proof someone else wrote. Use it even when the check looks simple enough to answer directly, because a wrong formalization produces exactly the same green `lake build` and the same plausible-looking statement as a right one. For auditing prose, docstrings, or LaTeX against the code, use lean-latex-sync instead.
- ▌