A proof for 3cubes is ready
-
https://github.com/expln/metamath-theorems/blob/master/metamath-christmas-challenge-2023/metamath-christmas-challenge-2023.mm
-
Igor
On Monday, December 18, 2023 at 4:59:54 PM UTC+1 savask wrote:
> Thierry,
>
> > Maybe I'll have another go at implementing the
On Mon, Jan 1, 2024 at 6:43 PM Jim Kingdon wrote:
> One (historical?) note: some of what we have now is the result of
> experimentation in the opposite direction - trying to figure out whether a
> logical system can be built without distinct variable constraints at all (I
> think there is some
This isn't something I'm likely to get hugely involved with myself, but
it does intrigue me particularly from the point of iset.mm. There right
now we have both https://us.metamath.org/ileuni/ax-bndl.html and
https://us.metamath.org/ileuni/ax-i12.html (stronger and weaker forms of
what in
> On Dec 31, 2023, at 7:32 PM, Jerry James wrote:
>
> Greetings,
>
> Due to some real life events, I had to step away from metamath last year.
> First, I want to apologize for ghosting the community on the last couple of
> pull requests I made in 2022. I hope you can forgive me for that.
In the last few days, I've been working on reducing the usage of ax-13,
aiming at getting the highest result with the minimum amount of changes.
The results of my findings are committed in my repository branch
https://github.com/GinoGiotto/set.mm/tree/ax-13-complete, which is based on
a
