[Lean Squad] feat(fv): Task 9 — CI skip guard + FVSquad/ directory scaffold

[github-actions]

🔬 Lean Squad — formal verification CI automation improvement.

What

Two small but important quality-of-life improvements to the Lean 4 formal verification setup:

1. CI skip guard for lake build

Added a "Check for Lean source files" step before lake build in .github/workflows/lean-proofs.yml.

When no *.lean files exist under FVSquad/, the workflow now prints an informational message and skips the build entirely. This avoids:

• Downloading and building Mathlib (~2 GB of compiled Lean artifacts)
• Wasting CI minutes during the Phase 2 → Phase 3 transition period

When .lean files do exist, the build runs as before.

2. FVSquad/ directory scaffold

Created formal-verification/lean/FVSquad/.gitkeep so the target directory is tracked in git now. The first real file to land here will be ArgumentArity.lean (Task 3).

Also updated the README.md status section to reflect the current Phase 2 state and the new directory.

Why now

Task 3 (writing ArgumentArity.lean) has been blocked on two consecutive runs because the runner's network firewall and bash allow-list prevent curl from downloading elan (the Lean toolchain installer). Until Lean is available in the runner, the CI workflow was triggering a multi-GB Mathlib download every time a PR touched formal-verification/lean/ — for zero verification benefit.

The skip guard makes this a non-issue.

Files changed

File	Change
.github/workflows/lean-proofs.yml	Add skip-when-no-lean-files guard step
formal-verification/lean/FVSquad/.gitkeep	New — scaffold the output directory
formal-verification/lean/README.md	Update status section

Verification

No Lean execution required for this PR — the changes are CI YAML and directory scaffolding only.

---

🔬 Lean Squad — Task 9: CI Automation | Run #24918627140 | 2026-04-25

---

Warning

Protected Files — Push Permission Denied

This was originally intended as a pull request, but the patch modifies protected files. A human must create the pull request manually.

Protected files

• .github/workflows/lean-proofs.yml

The push was rejected because GitHub Actions does not have workflows permission to push these changes, and is never allowed to make such changes, or other authorization being used does not have this permission.

Create the pull request manually

# Download the patch from the workflow run
gh run download 24918627140 -n agent -D /tmp/agent-24918627140

# Create a new branch
git checkout -b lean-squad/task9-ci-2026-04-25-2e42d667adee7a6c main

# Apply the patch (--3way handles cross-repo patches)
git am --3way /tmp/agent-24918627140/aw-lean-squad-task9-ci-2026-04-25.patch

# Push the branch and create the pull request
git push origin lean-squad/task9-ci-2026-04-25-2e42d667adee7a6c
gh pr create --title '[Lean Squad] feat(fv): Task 9 — CI skip guard + FVSquad/ directory scaffold' --base main --head lean-squad/task9-ci-2026-04-25-2e42d667adee7a6c --repo microsoft/testfx

Generated by 📐 Lean Squad, see workflow run.