• We will use Github for version control and for sharing files.
  • Register an account (free).
  • Watch some youtube videos to learn how to use Github.
  • Don't worry, I will assist you throughout this learning process.
• It would be a big plus if you can start using neovim as your text editor.
  • Start building your own neovim setup from scratch.
  • It is always helpful to check others' configs, for example, my LazyVim setup for academic writing (LaTeX, Markdown).
• Learn some languages including:
  • Mathematica (Wolfram)
  • Python
  • Tikz/PGF (draw figures in LaTeX)
  • Bash script if you use Linux or Mac OS.
  • You may use an AI assistant (Claude, ChatGPT, Gemini, ...) to help you learn these languages.
• Use biber for LaTeX references.
• You will not regret the effort that you have spent on the above technical aspects.

• Check out: the Student Guide for AI 2025.
• Use AI as a collaborator that must show its work, not as an oracle. Every mathematical claim an AI makes
  has to be checked: by you, against the source paper, by a computation, or (best) by a proof assistant.
• Get used to working with AI agents in the terminal (e.g. Claude Code, Codex, OpenCode), which can read
  your files, run LaTeX, and commit to git -- they fit naturally into the Github + neovim workflow above.

• The idea (see Andrej Karpathy's "LLM wiki" note):
  instead of asking an AI to re-read a pile of PDFs every time, have it build and maintain a linked
  collection of plain Markdown pages -- one page per paper, concept, method, or open problem.
• Our group keeps such a wiki for stochastic PDEs (about the papers we read and the techniques we use).
  It is private; group members get access on request.
• Ground rules that make a wiki trustworthy:
  • Read papers from their LaTeX source (arXiv), not from PDF text extraction -- formulas survive.
  • Every page cites its sources (citation keys, theorem numbers); no unsourced claims.
  • Plain text + git: the wiki is diffable, reviewable, and never locked in one tool.
• Start your own: a folder of Markdown notes under git is enough. Tools such as
  Obsidian or vimwiki can browse it.

• A skill is a short Markdown file of instructions (plus optional scripts) that an AI agent loads when
  a task matches -- e.g. "how we add a reference to the bibliography", "how we compile and check a paper",
  "how we write a referee report".
  • Overview: Agent Skills (Anthropic docs)
    and the open standard at agentskills.io.
  • A good public collection to study: superpowers
    (verification before claiming done, systematic debugging, writing plans).
• Why it matters: each time the AI (or you) makes a mistake, write the lesson down as a skill, so it does
  not happen again. Over time your skills become a record of how your research is done.
• I maintain several hundred such skills for our research workflow (literature, LaTeX, refereeing,
  Lean verification); I will share the relevant ones with you.

• Lean 4 is a proof assistant: a proof that compiles is checked by a small
  trusted kernel. Together with AI, this is how we make sure an argument is actually correct.
• Entry level (in this order):
  1. Natural Number Game -- in the browser, no installation.
  2. Mathematics in Lean -- the standard textbook for mathematicians.
  3. Theorem Proving in Lean 4 -- the language itself.
  4. Install Lean locally (works well with neovim or VS Code).
• Daily tools:
  • Lean 4 web editor for quick experiments.
  • Mathlib docs and Loogle to find lemmas.
  • Lean Zulip -- a very friendly community; ask questions there.
  • More: Learning resources (leanprover-community).
• Verifying papers with lean-pkg:
  • lean-pkg is a registry and trust gate for Lean 4 formalization packages: it records which packages
    exist, who works on each, and the evidence (receipts) that binds a package to a verified commit.
  • Before starting a new formalization, search the registry for prior art. Nothing becomes public
    without two receipts, and the second one is re-derived independently from the bytes.
  • Start with Start here, then
    How to. Source: github.com/lean-pkg/lean-pkg.
  • An example of a paper's companion formalization: total-coloring-lean.