Spring 2026 community call - Tue March 24 9:30-10:30 Central

[StevenClontz]

Cross posted to Zulip: #pi-base > Spring 2026 community call

Hi all, it's been some time, but we have a few new active community members and there are things to discuss, so I'd like to organize a community call.

Complete the survey at https://www.when2meet.com/?35476202-F9XVc with your availability and I'll try to find a mutually agreeable time.

[StevenClontz]

Based on that survey and my own availability, let's meet 9:30-10:30 Central time on Tuesday March 24. (Local time conversion in #pi-base > Spring 2026 community call @ 💬)

[StevenClontz]

Agenda:

1. Brief introductions
2. Funding search updates
3. Tracking subspaces, see Tracking subspaces and gaining traits #1678 (and some older threads)
4. Tracking independence of ZFC and possible use of alternative deduction, see Add "undecidable" truth value web#235 and https://code4math.zulipchat.com/#narrow/channel/416467-pi-base/topic/Deduction/with/579374842
5. Lean linkage, see https://code4math.zulipchat.com/#narrow/channel/416467-pi-base/topic/Lean.20linkage/with/577781024
6. New database using pi-Base model: https://catdat.app/ (from maker of https://ringtheory.herokuapp.com/ )

[prabau]

what's the zoom url?

[felixpernegger]

@StevenClontz

[StevenClontz]

https://zoom.us/j/93833246214 -- see you in 45 min

[prabau]

I misrepresented something in the meeting regarding the use of metaproperties for Kolmogorov quotients. @mathmaster13 asked if for this to apply a space $X$ would need to have its Kolmogorov quotient also in the database. The answer is no.
The Kol. quotient metaprops provide a way to virtually generate theorems associated to existing theorems, independently of any space. Or equivalently, it allows to derive traits on the fly based on the Kol. quotient metaprops.

For a simple example, suppose we have a space $X$ satisfying properties A and B, and the space is not $T_0$. One can then form the Kol. quotient $X'$ of $X$. And suppose we have metaprops of the form [ X is A => X' is A' ] and similarly for B, B'.
We can then deduce that X' is A' + B'. If pi-base has a theorem of the form [ A' + B' => C' ], we can the infer that X' satisfies C'.
And finally, if there is a another metaprop saying [ X' is C' => X is C ], we can finally conclude that X is C.
(Note: Often the metaprop for Kol. quotient is an iff. I phrased the metaprops above as going in a single direction at a time because sometimes they are not an iff.)

The trick would be to organize this in some systematic way to be able to take advantage of it.