---

license: apache-2.0
base_model: openbmb/MathForm-8B
tags:

- mlx
- math
- lean
- lean4
- formalization
- qwen3
- apple-silicon

---

# MathForm-8B-MLX-6bit

6-bit MLX conversion of `openbmb/MathForm-8B` for Apple Silicon.

This is the balanced variant between the smaller 4-bit build and the higher-precision 8-bit build.

## Quantization

- MLX-LM: 0.31.3
- Quantization: 6-bit
- Group size: 64
- Effective weight precision: 6.500 bits/weight
- Model size: ~6.3 GB
- Stored as 7 safetensors shards

## Local validation

Tested on:

- Apple M3 Pro
- 18 GB unified memory
- Python 3.12.14
- MLX 0.32.2
- MLX-LM 0.31.3

Validation prompt:

> For all real numbers x and y, if x = y then x^2 = y^2.

Result:

```lean
import Mathlib.Data.Real.Basic

theorem my_favorite_theorem :
    ∀ x y : ℝ, x = y → x ^ 2 = y ^ 2 := by sorry
```

Performance:

- Prompt processing: 144.983 tokens/s
- Generation: 19.977 tokens/s
- Peak unified memory: 6.866 GB

Autoformalization validation: PASS

## Usage

```bash
mlx_lm.generate \
  --model <model-path> \
  --prompt "Please convert the following informal math problem to a formal one in Lean 4 with a header. Use the following theorem names: my_favorite_theorem.

For all real numbers x and y, if x = y then x^2 = y^2." \
  --max-tokens 4096 \
  --temp 0.6 \
  --top-p 0.95
```

## Notes

MathForm is primarily an autoformalization model. Generated Lean code may contain `sorry` as a proof placeholder.

See `openbmb/MathForm-8B` for upstream architecture, training details, benchmarks, intended use, and limitations.

## License

Apache-2.0, following the upstream model.