[Lean Squad] feat(fv): CI improvement — skip lake build when no .lean files; create FVSquad scaffold

[github-actions]

Summary

This PR makes two incremental improvements to the Lean Squad formal verification infrastructure:

1. CI workflow improvement (lean-proofs.yml)

Add a pre-build check that counts .lean source files in FVSquad/. If none are present, the lake build step is skipped with an informative message. This prevents:

• Spurious Mathlib dependency downloads (~GB) on every CI run that touches the lean directory
• False-positive CI failures while no source files have been added yet
• Unnecessary build time wasted before any proofs exist

The check outputs a lean_count step output; the build step is conditioned on lean_count != '0'.

2. FVSquad/ directory scaffold

Create formal-verification/lean/FVSquad/ with a .gitkeep so the expected directory layout is present before .lean files are added in a future PR.

3. Docs / metadata

• Update TARGETS.md: mark ArgumentArity Phase 2 as complete (PR [Lean Squad] feat: formal verification infrastructure — research & CI automation #7799 merged).
• Update lean/README.md to describe the skip-build behaviour.

---

Task 9: CI Automation — status

The CI workflow exists (lean-proofs.yml, added in PR #7799, now merged). This PR applies a focused improvement to make the workflow robust for the empty-library period.

Task 3 (Formal Spec Writing for ArgumentArity) is blocked this run: the Lean toolchain (elan) could not be installed because the runner's network firewall blocked outbound connections to github.com. Per the hard requirement, no .lean files are committed without successful lake build verification. The formal spec will be written in a future run once network access is available.

---

🔬 Lean Squad — automated formal verification agent. This PR was opened by the Lean Squad CI agent. Changes are incremental infrastructure improvements; no Lean source code is included.

---

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 24900365706 -n agent -D /tmp/agent-24900365706

# Create a new branch
git checkout -b lean-squad/ci-and-task3-2026-04-24-4033cf6f5fe2822a main

# Apply the patch (--3way handles cross-repo patches)
git am --3way /tmp/agent-24900365706/aw-lean-squad-ci-and-task3-2026-04-24.patch

# Push the branch and create the pull request
git push origin lean-squad/ci-and-task3-2026-04-24-4033cf6f5fe2822a
gh pr create --title '[Lean Squad] feat(fv): CI improvement — skip lake build when no .lean files; create FVSquad scaffold' --base main --head lean-squad/ci-and-task3-2026-04-24-4033cf6f5fe2822a --repo microsoft/testfx

Generated by 📐 Lean Squad, see workflow run.