It would be handy to have a third option on the Space views to view All traits, rather than toggling between Asserted and Deduced.

• Ensure that the preview breaks at boundaries when possible (e.g. includes an entire inline math token or sentence, if reasonable)
• Better estimate of "length" for inline math tokens.

• Disprove "T3 + ~T2"
• Don't error on "T2 + ~T2"

• By text
• By formula
• Where unknown ...

Currently Logout link is non-functional.

When clicking around traits for a space, there is a race condition with TeXifying that causes the property name to be hidden sometimes.

For now, let users express "I only ever care about T_2 spaces". Eventually this should expand to let the user specify which axiom set they are working in.

If a user searches for T3 + ~T2, they should get a proof demonstrating why that's impossible. (If they run a search that we have no results for, but that we can't rule out, they should see some copy illustrating that.)

Once the viewer has the audited data including references, they should be linked to using the following syntax:

• MR: https://www.ams.org/mathscinet-getitem?mr={{id}} (even if the user doesn't have access to MathSciNet, this still pulls up a minimal page with a full citation)
  • e.g. {{mr:MR0266131}} becomes https://www.ams.org/mathscinet-getitem?mr=MR0266131
• DOI: https://doi.org/{{id}} (NOT www.doi.org)
  • e.g. {{doi:10.1007/978-1-4612-6290-9}} becomeshttps://doi.org/10.1007/978-1-4612-6290-9
• Wikipedia: https://en.wikipedia.org/wiki/{{id}}
  • e.g. {{wikipedia:10.1007/Counterexamples_in_Topology}} becomes https://en.wikipedia.org/wiki/Counterexamples_in_Topology

We should have some mechanism for spotting broken links. Easiest thing is probably to send any routing errors to Rollbar.

Much of src/models/Store should probably be in src/queries, or pushed down into @pi-base/core for reuse.

Right now many (but not all) tables are sortable by clicking on the header, but that behavior isn't terribly visible or well-tested.

When compiling on Linux, yarn run start emits the following error:

./src/routes.tsx
(9,22): error TS2307: Cannot find module './components/Property'.

It appears that it is looking for src/components/Property/index.tsx but the file in the repository is actually named Index.tsx, with a capital I. Renaming it to index.tsx fixes the error. Then I had to do the same for src/components/Theorem/Index.tsx.

Are you folks developing on a case insensitive OS and so never saw this, or is something else wrong?
I could create a pull request to just git mv the two files, but not sure if that is really the proper fix.

We currently pre-check the bundle for contradictions before saving it, so this should be impossible. But we probably should have well-defined error handling here in any case.

It's currently convenient for the CI server, but really doesn't need to be cluttering up the repo

We should make it as easy as possible to review PRs into pi-base/data. This will be an ongoing effort, but may include:

• A diff view across bundles
• Better linking from a viewer looking at a non-master bundle back to the repo
• CI task to add links from the repo to a viewer instance

• Error monitoring
• Better onboarding material / links to Github
• Domain re-routing
• Newsletter

There's enough deduction machinery in place that we shouldn't have to manually tag converses any more.

There are a small number of places where we're using the any type for external libraries. We should declare (and contribute back) proper typings for those.

I always liked Rudin's review of Counterexamples. I think an paraphrased excerpt like the one below would be a nice addition to the front page of the viewer.

To paraphrase Mary Ellen Ruden in her review of Counterexamples in Topology, topology is a dense forest of counterexamples, and a usable map of the forest is a fine thing. The pi-Base team hopes that researchers will benefit from the organization and uniformity provided by the pi-Base, and that mathematicians and students exploring new branches of topology will benefit from having the pi-Base as a guide.

We should accept Math Overflow and Math.StackExchange citations; part of the review process would be to reject downvoted solutions.

Underscores and italics are going to be an issue. See: https://pi-base.firebaseapp.com/theorems/I000029

Given a collection of spaces (say, with a known property), it would be nice to compare the traits that those spaces have in common.

When on a non-audited branch, users should be able to create and edit spaces, properties, theorems and traits

Move toggling master/user branches to the toolbar, including changing the toolbar color to reflect its status.

We eventually want to support full-on automated theorem prover integration, but would it be possible to model a handful of simple relationships between spaces ("is a (closed) subspace of", "is a product of")?

that isn't the react default

Should probably redirect to a standard UID-route but could accept slugs or names where possible.

We can improve the page for displaying deduced theorems and add

• a visualization
• an option to start with the proximal deduction and expand back as desired

Search urls should be shareable

Right now there is an Add button when viewing Related theorems on http://viewer.counterexamples.info/properties/P100052 in the master branch.

The design is stable enough now that the query / action / reducer layer should be well-tested. Testing the component layer honestly doesn't seem that bad either ...

Filtering properties down to "Haus" should show T_2 in the list of results

Currently the deduction engine has a rule for perfectly normal implying T4. Via some other deductions pi-base then deduces T1. However, in general perfectly normal (as defined in Wikipedia and in Pi-base) does not imply T1 or T2. The reason is that without the T1 axiom it is not known whether singletons are closed. It would be nice if the T1 and perfectly normal properties were independent.

One use case: a professor starts a branch, but wants their student to add references. It would be ideal if the student got credit for those commits and didn't have to have the professor's login.

Viewer development has moved over to pi-base/server, but we don't want to lose these issues.

It would be nice to have a unified search experience that

• Included results across resource types
• Included results by formula, iff the input parses as a formula. (We'd need to figure out what to do with singe-term searches though, as those always parse as an atom.)