AI task runner

[jstoobysmith]

Create physlib_ai_tasks

This issue was drafted with the help of Claude Opus 4.8.

A small tool with two requirements:

1. List open tasks in [Physlib](https://github.com/leanprover-community/physlib) that are suitable for
   an LLM coding agent to work on.
2. Help set up an agent on a chosen task — either by launching the agent directly, or by emitting a
   ready-to-paste prompt.

Overriding goal: make it as easy as possible for someone to start running these tasks. Minimal setup,
go from "how can I contribute with an AI?" to "an agent is working on it" in as few steps as possible.

Relation to TauCetiWorker

This tool and [kim-em/TauCetiWorker](https://github.com/kim-em/TauCetiWorker) share the same starting
point: survey the available work, then launch an agent on a chosen item. TauCetiWorker layers a lot of
autonomous-operation machinery on top of that; this tool stops at those two steps. The lists below spell out
what is shared and what is deliberately left out.

Same as TauCetiWorker:

• Surveys/lists the available work (TauCeti's dashboard / status). → requirement 1
• Launches an agent on a chosen item, or copies the command/prompt instead of running it (TauCeti's
  Enter/number to run, c to copy). → requirement 2
• Bring-your-own-agent / agent-agnostic.
• Hardwired to one project (physlib) rather than being a general framework.

Does not try to replace (TauCetiWorker features left out):

• The autonomous --loop driver that picks and runs work unattended.
• Sandboxing (bubble / Incus).
• Quota pacing against a subscription.
• Multi-worker coordination (branch claims, safe-push, etc.).
• PR-lifecycle tending: review, fix-CI, fix-from-review, rebase, Mathlib bump.
• Any action on PRs themselves (merge, close, de-duplicate).

Task list

The kinds of task to surface:

1. Close a semiformal_result — the statement is already formally typed; fill in the missing proof.
2. Formalize an informal_lemma — turn a prose lemma into a formal statement and proof.
3. Formalize an informal_definition — turn a prose definition into a formal one.
4. Resolve a tagged TODO — carry out a tagged to-do item.
5. Close a sorry — fill in a proof hole so the file builds with no sorry.
6. Align documentation with the heading standard — reformat module/file documentation to follow the
   # A. …, ## A.1. …, … hierarchical heading convention.
7. Bring ./QuantumInfo up to standard — improve the format of files under QuantumInfo/ to match
   Physlib standards and pass the linters.
8. Golf / shorten an existing proof — replace a long proof with a shorter one that still builds.

Potential implementation

• Write a prompt file for each of the different task types above. Each prompt encodes how to do that kind of
  task: the relevant context, the physlib conventions to follow, the build/lint commands, and the acceptance
  criterion. Both modes of requirement 2 reuse these — launching an agent directly gives it the matching
  prompt file, and the "emit a prompt" mode prints it.

[jstoobysmith]

I think the starting point of this is to define an inductive type

inductive Tasks 
   | todo (id : String) : Tasks
   | golf (name : Name) : Tasks
   | review (nat : Nat) : Tasks 
   | fixLint (name : Name) : Tasks
   | ...