---
language:
- en
license: apache-2.0
tags:
- lean4
- theorem-proving
- verification
- code-verification
- mlx
base_model: Goedel-LM/Goedel-Code-Prover-8B
pipeline_tag: text-generation
library_name: mlx
---

# abalogh/Goedel-Code-Prover-8B-8bit

This model [abalogh/Goedel-Code-Prover-8B-8bit](https://huggingface.co/abalogh/Goedel-Code-Prover-8B-8bit) was
converted to MLX format from [Goedel-LM/Goedel-Code-Prover-8B](https://huggingface.co/Goedel-LM/Goedel-Code-Prover-8B)
using mlx-lm version **0.31.1**.

## Use with mlx

```bash
pip install mlx-lm
```

```python
from mlx_lm import load, generate

model, tokenizer = load("abalogh/Goedel-Code-Prover-8B-8bit")

prompt = "hello"

if tokenizer.chat_template is not None:
    messages = [{"role": "user", "content": prompt}]
    prompt = tokenizer.apply_chat_template(
        messages, add_generation_prompt=True, return_dict=False,
    )

response = generate(model, tokenizer, prompt=prompt, verbose=True)
```