Zulip Chat Archive

Stream: triage

Topic: PR #10645: feat(combinatorics/additive/small_roth): Small...

Random Issue Bot (May 12 2022 at 14:22):

Today I chose PR 10645 for discussion!

feat(combinatorics/additive/small_roth): Small Roth numbers
Created by @Yaël Dillies (@YaelDillies) on 2021-12-06
Labels: awaiting-author

Is this PR still relevant? Any recent updates? Anyone making progress?

Yaël Dillies (May 12 2022 at 14:24):

This PR is a bit weird on its own because it does not end with a clear result. Instead, it sets up the invariant of an algorithm that could then be used by tactics to calculate Roth numbers.

Yaël Dillies (May 12 2022 at 14:25):

The only thing that's missing from this PR to make it enjoyable is a demonstration of a Roth number calculation using the two lemmas.

Yaël Dillies (May 12 2022 at 14:26):

@Bhavik Mehta, @Eric Wieser and I discussed it already

Random Issue Bot (Jul 23 2022 at 14:13):

Today I chose PR 10645 for discussion!

feat(combinatorics/additive/small_roth): Small Roth numbers
Created by @Yaël Dillies (@YaelDillies) on 2021-12-06
Labels: awaiting-author

Is this PR still relevant? Any recent updates? Anyone making progress?

Random Issue Bot (Dec 11 2022 at 14:08):

Today I chose PR 10645 for discussion!

feat(combinatorics/additive/small_roth): Small Roth numbers
Created by @Yaël Dillies (@YaelDillies) on 2021-12-06
Labels: awaiting-author

Is this PR still relevant? Any recent updates? Anyone making progress?

Yaël Dillies (Dec 11 2022 at 17:40):

I set myself to write the aforementioned tactic. Probably it's not too hard.

Last updated: Dec 20 2023 at 11:08 UTC