Zhangir Azerbayev

feat(group/perm/sign): swap_adj_induction_on

4

1) Defines the multilinear map that sends a tuple of elements of an algebra to their product. 2) ~~Defines the typeclass `alternating_map` that extends `multilinear_map`.~~ Superseded by #5102 3) Proves...

Python package

2

Adds python interface via a package called `pylean`. See `README.md` for usage instructions. Unit tests in `pylean/tests`.

Iterative execution of proofs

2

A common use case for the `repl` is writing proofs tactic by tactic. Currently, this requires re-executing the entire head of the source file. It would be great if we...

Local inference with llama.cpp

5

This PR adds support for an inference server powered by [llama.cpp](https://github.com/ggerganov/llama.cpp) that runs efficiently on CPU. I am able to get a tactic suggestion in a few seconds on my...

Being able to run `tactic_benchmark` on decls that use `sorry` is rather useful. For example, when benchmarking tactics on evaluations such as MiniF2F which don't come with proofs for every...