MathForm-8B-MLX-4bit

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

MathForm-8B is focused on mathematical autoformalization and Lean 4. This conversion reduces memory and storage requirements for local MLX inference.

Quantization

• MLX-LM: 0.31.3
• Quantization: 4-bit
• Group size: 64
• Effective weight precision: 4.500 bits/weight
• Model size: ~4.3 GB

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:

import Mathlib.Data.Real.Basic

theorem my_favorite_theorem {x y : ℝ} (h : x = y) :
    x ^ 2 = y ^ 2 := by sorry

Performance:

• Prompt processing: 183.786 tokens/s
• Generation: 27.155 tokens/s
• Peak unified memory: 4.839 GB

Autoformalization validation: PASS

Usage

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.