LICENSE file does not match the source

[eric-wieser]

This header says that the LICENSE is apache 2.0, copyright Open AI

miniF2F-lean4/MiniF2F/Test.lean

Lines 1 to 7 in 76ab47e

	/-
	Copyright (c) 2021 OpenAI. All rights reserved.
	Released under Apache 2.0 license as described in the file LICENSE.
	Authors: Kunhao Zheng, Stanislas Polu, David Renshaw, OpenAI GPT-f
	! This file was ported from Lean 3 source module valid and edited by Kaiyu Yang.
	-/

but the license file in the repo says

miniF2F-lean4/LICENSE

Lines 1 to 3 in 76ab47e

	MIT License
	Copyright (c) Meta Platforms, Inc. and affiliates.

Presumably this needs to be distributed under a concatenation of both licenses, if Meta is claiming copyright on the corrections?

[yangky11]

This issue was probably inherited from https://github.com/facebookresearch/miniF2F, as the earliest version of this repo was translated from facebookresearch/miniF2F using mathport. The translation was done before I joined Meta. Given that the repo is under my personal account (not managed by Meta), I should probably use my name for the repo's license and put Meta's license in individual Lean files (together with OpenAI's license.) Any suggestions are welcome!