> You are prohibited from ... Using Output to develop models that compete with OpenAI.
If this were a software license, it'd surely be classified as nonfree.
> You are prohibited from ... Using Output to develop models that compete with OpenAI.
If this were a software license, it'd surely be classified as nonfree.
Thinking another layer deep, though, if someone used OpenAI tools to develop software that then later got used to compete with OpenAI, surely it would fully workaround this already unenforceable ToS restriction anyways, right?
> “Specifically, we initialized the DeepSeek-Prover using the DeepSeekMath-Base 7B model (Shao et al., 2024). Initially, the model struggled to convert informal math problems into formal statements. To address this, we fine-tuned the DeepSeek-Prover model using the MMA dataset (Jiang et al., 2023), which comprises formal statements from Lean 4’s mathlib2 that were back-translated into natural language problem descriptions by GPT-4. We then instructed the model to translate these natural language problems into formal statements in Lean 4 using a structured approach.”
Section 3.1 in https://arxiv.org/html/2405.14333v1