aiprover-119b

AIProver is a 119B-parameter mixture-of-experts language model (about 6B active parameters per token) for Lean 4 theorem proving and proof auto-formalization.

Details

• Architecture: 36 layers, 128 routed experts plus 1 shared expert, 4 experts per token
• Weights: FP8 (e4m3), Mistral consolidated format (consolidated-*.safetensors, params.json, tekken.json)
• Context length: up to 1,048,576 tokens

License

Released under the GNU Affero General Public License v3.0 (see LICENSE). The model builds on an Apache-2.0 licensed model; its terms are respected. Training and harness code will be released separately.