Draft: Bump Lean version to 4.28.0-rc1

[protoben]

This is an attempt to bump the Lean version to take advantage of some recent performance improvements in Lean. We change the Lean version in all lean-toolchain files, as well as the cslib and mathlib dependencies in the various lakefile.toml files.

Note that this is built on top of #11.

[protoben]

I'm able to run lake build successfully in the zkLean directory, but when I try to run it in the examples directory, I get this error from BVModEq:

error: BVModEq/SolveMLE.lean:182:11: Application type mismatch: The argument
  idSyn
has type
  TSyntax `ident
but is expected to have type
  TSyntax `Lean.binderIdent
in the application
  idSyn.raw
error: BVModEq/SolveMLE.lean:196:11: Application type mismatch: The argument
  idSyn
has type
  TSyntax `ident
but is expected to have type
  TSyntax `Lean.binderIdent
in the application
  idSyn.raw
error: Lean exited with code 1
Some required targets logged failures:
- BVModEq.SolveMLE
error: build failed

[Ptival]

I have updated the PR wrt. the changes I merged in main earlier today.

I have a fix that makes BVMod type-check again.

However, some of Liza's proofs are failing, and they might take a lot of time to figure out. I think we should probably merge, and only fix these proofs if we need them.

@jprider63 @protoben

[jprider63]

Hmm if the proofs fail I would prefer to hold off on bumping Lean versions until we have time to fix them. We don't need the latest Lean version right now do we?

[protoben]

Hmm if the proofs fail I would prefer to hold off on bumping Lean versions until we have time to fix them. We don't need the latest Lean version right now do we?

Yes, that makes sense to me. Let's hold off. I'll go ahead and revert to the old version in the Jolt PR.

@jprider63 Do you think it would be better to keep this MR as is in draft status, or to close it and start a new one once we want to update? Happy either way.

[jprider63]

I'd say we leave it open as a draft PR.

For the Jolt PR, it's likely fine that it points to the commit on this branch since that currently builds.