add news items

[icecream17]

The latest entry in https://us.metamath.org/mpeuni/mmrecent.html section "Recent news items" is on 7-Aug-2021

So perhaps its time to add new entries (as noted somewhere in the discussion group or issues, can't find it)

Some ideas:

• ax-13 usage reduced to 1%
• several improvements by Samiro Discher in https://us.metamath.org/mmsolitaire/pmproofs.txt
• metamath-lamp tool (ooh, it now has macros)

[jkingdon]

Suggestion:

• (1-Jul-2023) There is now a $j usage directive which can be used to specify that certain axioms are not used (directly or indirectly) in the proof of a given theorem. Metamath-knife enforces this when passed the -u option.

[tirix]

Should we celebrate new contributors? Like @metakunt @ProgramCrafter @zwang123 and @CatsAreFluffy
Also @sctfn makes a big comeback after 2 years away :)

[jkingdon]

Should we celebrate new contributors? Like @metakunt @ProgramCrafter @zwang123 and @CatsAreFluffy Also @sctfn makes a big comeback after 2 years away :)

I suppose and if so let's not forget @BTernaryTau whose contributions on the use of the axiom of power sets have been extensive, and interesting because one of the hot topics these days is on predicative versus impredicative theories (maybe not in the exact context of ZF minus power set, but it seems likely to have some relationship).

[tirix]

...and now there's also the "Advent of Metamath 2024" initiated by @savask (and the 2023 version if we missed it in the news) : so many news!