THIRD-PARTY LICENSES
====================

open-atp itself is distributed under the MIT License (see LICENSE). It
incorporates and/or distributes code from the following open source projects,
which retain their own licenses:

================================================================================

1. ax-prover
   Upstream:  https://github.com/Axiomatic-AI/ax-prover-base
   Fork used: https://github.com/henryrobbins/ax-prover-base

   GNU Affero General Public License, Version 3 (AGPL-3.0-only)

   Copyright (c) Axiomatic-AI (Borja Requena, Austin Letson, Krystian
   Nowakowski, Izan Beltran Ferreiro, Leopoldo Sarra, and contributors).

   open-atp does not link against or import ax-prover in-process. It is
   installed in an isolated environment (pipx) and invoked at arm's length as a
   separate `ax-prover` CLI process; the open-atp sandbox image distributes
   that binary (see images/Dockerfile). This separation keeps open-atp's own
   MIT-licensed source unaffected by the AGPL's copyleft; the AGPL obligations
   below attach to the ax-prover component only.

   This program is free software: you can redistribute it and/or modify it
   under the terms of the GNU Affero General Public License as published by the
   Free Software Foundation, either version 3 of the License, or (at your
   option) any later version.

   This program is distributed in the hope that it will be useful, but WITHOUT
   ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS
   FOR A PARTICULAR PURPOSE. See the GNU Affero General Public License for more
   details.

   The full license text is available at https://www.gnu.org/licenses/agpl-3.0.txt
   and in the LICENSE file of the source repositories above.

   Source offer (AGPL sections 6 and 13): the complete corresponding source for
   the version of ax-prover distributed by open-atp -- including the local
   modifications carried by the fork -- is publicly available at the fork URL
   above. The exact revision distributed is pinned as AX_PROVER_REF in
   images/Dockerfile and src/open_atp/__main__.py. Where open-atp is operated
   as a network service, this notice and that repository constitute the offer of
   source required by AGPL section 13 for users interacting with ax-prover
   remotely.

================================================================================

2. numina-lean-agent
   Upstream: numina-lean-agent

   MIT License

   The skills and prompts under vendor/numina/ are copied (and lightly adapted)
   from the upstream numina-lean-agent project; see vendor/numina/VENDOR.md for
   provenance, the copied commit, and the adaptations applied. Upstream ships no
   LICENSE file but declares MIT in its README, so the standard MIT text is
   reproduced below with attribution to the upstream authors.

   Copyright (c) 2026 Numina (numina-lean-agent authors)

   Permission is hereby granted, free of charge, to any person obtaining a copy
   of this software and associated documentation files (the "Software"), to deal
   in the Software without restriction, including without limitation the rights
   to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
   copies of the Software, and to permit persons to whom the Software is
   furnished to do so, subject to the following conditions:

   The above copyright notice and this permission notice shall be included in all
   copies or substantial portions of the Software.

   THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
   IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
   FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
   AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
   LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
   OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
   SOFTWARE.
