K2-Prover-SFT-8B-LORA

Merged 8B SFT model for Lean 4 theorem proving.

This repository contains the merged full model produced from:

• Base model: /scratch/joshua.ong/models/Qwen3-8B
• LoRA adapter: /scratch/joshua.ong/k2-diffusion-synthetic/LLaMA-Factory/saves/qwen3-8b/lora_clean/difflean_sft_ds2_test/checkpoint-7036
• Merge config: examples/merge_lora/k2_prover_sft_8b_lora.yaml

The LoRA weights have been merged into the base model, so inference should load this as a standard Transformers causal language model without a separate adapter.