平行语料库是一个将一种语言的文本与另一种语言的对应文本配对的集合。

Isabelle 平行语料库 (IPC) 是一个由社区驱动的倡议，旨在创建 Isabelle 文档的平行语料库。 IPC 将 Isabelle 中的形式化文档（如定理、引理、定义等）与它们的自然语言对应文本配对。

IPC 中的条目具有多个级别的数据标注。在第一级别上，记录了文档（例如定理陈述）的自然语言陈述和自然语言源（例如教科书）。第二级别的标注将自然语言证明中的句子与相应的 Isabelle 证明脚本中的陈述配对。第三级别的标注允许将自然语言中的单词与 Isabelle 证明脚本中的标记对齐。