Shad Amethyst amethyst

1 Followers · 0 Following

• Alsace, France
• https://shadamethyst.xyz/
• Joined on Jul 01, 2022

Repositories Packages Public Activity Starred Repositories

Loading Heatmap…

amethyst pushed to main at amethyst/sort-image

• e6ba386e1b Clean code up a bit and document options a bit

7 months ago

amethyst pushed to main at amethyst/sort-image

• cf9eb41c17 🎉 First commit

7 months ago

amethyst created branch main in amethyst/sort-image

7 months ago

amethyst created repository amethyst/sort-image

7 months ago

amethyst pushed to amethyst at amethyst/semantics-2023

• 8d480a49c7 🎉 Finish exercises 9 (with IPM cheating)
• c4427f5f9c Merge remote-tracking branch 'exercises/main' into amethyst
• 04f1502ff5 release exercise 9
• a565eb10c3 solution for exercise 08
• Compare 4 commits »

11 months ago

amethyst pushed to laurent-lost-commits at amethyst/rubin-lean4

• def2e9c37c 💄 added Emilie to authors
• 3753948ac8 💥 tried to add rubin
• Compare 2 commits »

11 months ago

amethyst created branch laurent-lost-commits in amethyst/rubin-lean4

11 months ago

amethyst pushed to main at amethyst/rubin-lean4

• ee3cdfe13b :up_arrow: Upgrade mathlib

11 months ago

amethyst pushed to main at amethyst/rubin-lean4

• 253c33035d 🎉 Finished the proof of rubin's theorem

11 months ago

amethyst pushed to amethyst at amethyst/semantics-2023

• c0a9dcdb1c ✨ Start exercises 8

11 months ago

amethyst pushed to amethyst at amethyst/semantics-2023

• 010390ce97 Merge remote-tracking branch 'exercises/main' into amethyst
• 6cc382131f release exercise 8
• 1594ef0bd2 solution for exercise 07
• Compare 3 commits »

11 months ago

amethyst pushed to main at amethyst/rubin-lean4

• 8737257190 🎉 Construct the equivariant homeomorphism to the rubin space

11 months ago

amethyst pushed to main at amethyst/rubin-lean4

• 7d92d98b60 🎉 Finally reached the homeomorph stage!
• 7c5ce7e631 ✨ Working equiv for RubinSpace
• 6b2f21fec8 ✨ Fix all sorries
• 6a2f4960d7 ✨ Construct ultrafilters in the topolical space and rubinfilters from one another
• 5fb9162950 ✨ Prove that UltrafilterInBasis is a sufficient condition for convergence
• Compare 5 commits »

11 months ago

amethyst pushed to main at amethyst/rubin-lean4

• 431a2931d7 ✨ Implement UltrafilterInBasis.map_basis
• e84ff177bd ✨ Start working on Filter.InBasis
• 7b4307d76c ✨ Split apart the implications of theorem 3.5 to be able to use ultraprefilters
• Compare 3 commits »

11 months ago

amethyst pushed to amethyst at amethyst/semantics-2023

• 03665a3ebe ✨ Exercises 7

11 months ago

amethyst pushed to main at amethyst/rubin-lean4

• ec9587c7e9 🔥 Draft out the end of the proof
• 65e1ab7fc8 📝 Refactor RegularSupportBasis
• 60111656b8 ✨ Replace ContinuousMulAction with ContinuousConstSMul
• a87dc079d6 💩 Messy draft code to work towards the end of the proof
• Compare 4 commits »

11 months ago

amethyst pushed to main at amethyst/rubin-lean4

• 50b4b49932 ✨ Fully prove proposition 3.5

11 months ago

amethyst pushed to main at amethyst/rubin-lean4

• 24dd2c4f0a 🔥 New notation for RigidStabilizer and prove first lemma for proposition 3.5
• 522f345f34 ✨ Implement SMul on filters, prove compactness of smulImage and that orbit is a subset of support
• Compare 2 commits »

11 months ago

amethyst pushed to main at amethyst/rubin-lean4

• 23d0821290 ✨ Almost complete proof of proposition 3.5

11 months ago

amethyst pushed to amethyst at amethyst/semantics-2023

• 02b9ce9abb 📝 Add a few comments for paper proofs
• 82042039b9 Merge remote-tracking branch 'exercises/main' into amethyst
• cd222f11c5 added church encodings fully faithful
• 4f600972e5 release exercise 07
• d9bd2ee560 solution for exercises 06
• Compare 5 commits »

12 months ago