Junyan Xu

Could the ineffectiveness of black's rollouts be an artifact?

8

From [the paper](https://arxiv.org/pdf/1902.04522.pdf): > Intuitively, increasing the number of MCTS iterations (rollout count) improves the AI’s strength by exploring more of the game tree. Toward better understanding the rollout count’s...

a GAN idea

1

Thank you for the work. I recently start working on reinforcement learning of mathematical research (with the formal language and deduction system of a proof assistant as the environment); it's...

feat(set_theory/cardinal): cardinality of `multiset`, `polynomial` and `mv_polynomial`

4

+ Show `#(multiset α) = max (#α) ℵ₀` when `α` is nonempty. Show the same for `#(α →₀ ℕ)`, which is used in the mv_polynomial proof (see below). + Prove...

feat(data/*): `unique` instances for `dfinsupp` and `direct_sum`

11

+ Add `unique` instances when the codomain types are subsingletons and rename the original `unique` instances (which apply when the domain is empty) to `unique_of_is_empty`. These are in analogy to...

feat(ring_theory/localization/away): R[X]/(rX-1) as localization

5

I don't have any specific application in mind, and just wanted to test how hard it is to connect the two. For a general submonoid, adjoining the inverses of elements...

chore(*): restore `subsingleton` instances and remove hacks

1

#### Background The `simp` tactic used to [look for subsingleton instances excessively](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.235672.20breaks.20timeout/near/223034551), so every subsingleton/unique instances added to mathlib could slow down `simp` performance; in fact, removing some subsingleton instances...

feat(data): port finsupp.ne_locus/lex to dfinsupp

2

+ Add new files *dfinsupp/ne_locus* and *dfinsupp/lex* mostly by copying the finsupp counterparts and making trivial adaptions. Use the `dfinsupp` lemmas/constructions to golf the `finsupp` counterpart, e.g. the `linear_order` on...

feat: SuccOrder and recursion principle on well-ordered type

3

Order/SuccPred/Basic.lean: add `SuccOrder.ofLinearWellFoundedLT`, which puts a SuccOrder on an arbitrary well-ordered type. Also add the dual, `PredOrder` version. Add missing `pred` lemmas corresponding to existing `succ` lemmas. Order/SuccPred/Limit.lean: add `SuccOrder.limitRecOn`...

feat: cardinality of `Field.Emb` for infinite extensions

1

A construction by transfinite recursion, fairly standard in set theory, but I have yet to see similar arguments in mathlib. See [module docstring](https://github.com/leanprover-community/mathlib4/blob/Field_Card_Emb/Mathlib/SetTheory/Cardinal/FieldEmb.lean#L20-L137) for more details. I use some ad...

[Harrison-John.pdf](https://github.com/alreadydone/contents/files/9996347/Harrison-John.pdf)