Geoint

### Dataset Summary

**Geoint** is a comprehensive benchmark dataset explicitly designed for formal geometric problemsolving. Geoint encompasses 1,885 carefully curated geometric questions across diverse categories including plane, spatial, and solid geometry problems. Each problem is richly annotated with both structured textual descriptions and accompanying visual diagrams to support multimodal understanding. Furthermore, Geoint leverages the Lean 4 proof assistant to formally represent geometric elements and relationships, enabling rigorous and complete formal reasoning within a verifiable framework.

You can load the dataset using:

```python

from datasets import load_dataset

dataset = load_dataset("your-username/Geoint", split="train")

```

### Data Fields

| Field | Type | Description |
|------------------|-------------|-------------|
| `id` | `string` | Unique identifier for each problem |
| `question` | `string` | Text description of the geometric problem |
| `response` | `string` | Solution text and its corresponding Lean 4 code|
| `question_type` | `string` | Problem type: *Free* or *Proof* |
| `assistant_line` | `bool` | Whether auxiliary lines are needed for solving |
| `question_image` | `binary` | Problem diagram image (PNG format) |
| `assistant_image`| `binary` or `None` | Image with auxiliary lines (PNG format) |

### Citation Information

Please consider citing [our paper](https://arxiv.org/pdf/2508.03173) if you find this dataset useful:

```
@misc{wei2025geointr1formalizingmultimodalgeometric,
title={Geoint-R1: Formalizing Multimodal Geometric Reasoning with Dynamic Auxiliary Constructions},
author={Jingxuan Wei and Caijun Jia and Qi Chen and Honghao He and Linzhuang Sun and Conghui He and Lijun Wu and Bihui Yu and Cheng Tan},
year={2025},
eprint={2508.03173},
archivePrefix={arXiv},
primaryClass={cs.AI},
url={https://arxiv.org/abs/2508.03173},
}
```

### 数据集概述
**Geoint** 是专为形式化几何问题求解打造的综合性基准数据集。该数据集涵盖1885道精心甄选的几何问题，类别覆盖平面几何、空间几何与立体几何。每道问题均附带结构化文本描述与配套可视化图表，可支撑多模态理解任务。此外，Geoint借助Lean 4证明助手（Lean 4 proof assistant）对几何元素与几何关系进行形式化表示，能够在可验证的框架内实现严谨且完整的形式化推理。

你可以通过以下代码加载该数据集：
python
from datasets import load_dataset

dataset = load_dataset("your-username/Geoint", split="train")

### 数据字段
| 字段名 | 类型 | 描述 |
|-----------------|-------------|----------------------------------------------------------------------|
| `id` | 字符串 | 每道问题的唯一标识符 |
| `question` | 字符串 | 几何问题的文本描述 |
| `response` | 字符串 | 解题文本及对应的Lean 4代码 |
| `question_type` | 字符串 | 问题类型：分为*自由作答（Free）*与*证明题（Proof）* |
| `assistant_line`| 布尔值 | 求解该问题是否需要添加辅助线 |
| `question_image`| 二进制数据 | 问题配图（PNG格式） |
| `assistant_image`| 二进制数据或`None` | 带有辅助线的配图（PNG格式） |

### 引用信息
若您发现本数据集对您的研究有所助益，请引用[我们的论文](https://arxiv.org/pdf/2508.03173)：

@misc{wei2025geointr1formalizingmultimodalgeometric,
title={Geoint-R1: Formalizing Multimodal Geometric Reasoning with Dynamic Auxiliary Constructions},
author={Jingxuan Wei and Caijun Jia and Qi Chen and Honghao He and Linzhuang Sun and Conghui He and Lijun Wu and Bihui Yu and Cheng Tan},
year={2025},
eprint={2508.03173},
archivePrefix={arXiv},
primaryClass={cs.AI},
url={https://arxiv.org/abs/2508.03173},
}