RFC: lean-action for math projects

Stream: lean4

[Shreyas Srinivas]

Currently the lean4checker action in lean-action checks all of a project's dependencies when run on a project. This means it spends most of its time on mathlib. There also seems to be a persistent issue with proofwidgets. Is there a way to run the standard lean-action script to only check the project and avoid proof widgets?

[Shreyas Srinivas]

The proximate issues is this PR : https://github.com/teorth/equational_theories/actions/runs/11295435860/job/31418145134?pr=517

Here lean4checker is taking way too long and most of the checking happens on mathlib.

[Kim Morrison]

#17713 updates Mathlib to use a new version of lean4checker that by default only checks the current project.