TheorIC Labs 发布面向 Lean 4 的多提供商 AI 客户端

TheorIC Labs 创始人 Harsh Gupta 构建了 LeanLLM，旨在将模型 API 引入 Lean 原生类型，同时应用代码仍需对模型输出进行检查。

By · Published

Primary source: X

为何重要

LeanLLM 瞄准了正式的、带类型的应用代码与开发者越来越常调用的松散界定的模型 API 之间的空隙。它的承诺取决于 Lean 的检查在多大程度上覆盖模型响应周围的代码；这些检查并不验证模型的声明，也不能消除对外部输出谨慎处理的必要性。

TheorIC Labs builds a Lean 4 client for multi-provider AI calls — Founder Harsh Gupta's library wraps model APIs in Lean-native types, while leaving the hard question of reliable checks on model output to application code.

Harsh Gupta (@hargup13) 在 他于10月14日的公告中 表示 TheorIC Labs 发布了 LeanLLM，这是一个客户端库，允许 Lean 4 应用通过一个接口调用多个提供商的模型。该库包括工具调用、结构化输出、图像输入和流式传输；其重要性在于 Gupta 将熟悉的 AI 应用管道放置在一个以形式化证明和显式类型为核心的语言内部。

Gupta 通往 TheorIC 的路径贯穿了开源软件和初创公司。他的 个人简介 称他在 IIT Kharagpur 学习数学和计算机科学，参与过 SymPy 的贡献，并帮助打造了学生信息维基 MetaKGP。他还创立了 Felvin，一家他称已筹集 350,000 美元的 AI 搜索与应用初创公司。那家早期公司与 TheorIC 是分开的；上述融资数字不适用于 LeanLLM。…

When you purchase through links in our articles, we may earn a small commission. This doesn’t affect our editorial independence.

Reader comments

Conversation for this story loads after sign-in.