The formal-proof tag has no usage guidance.

**0**

votes

**1**answer

40 views

### Prove or disprove a monotonicity property of a certain convex optimization problem

Let $R = (r_{ij})$ be an $n\times k$ real matrix with only positive entries,
and consider the convex optimization problem
$\max f(x) = \sum_{i=1}^n \log \sum_{j=1}^k r_{ij} x_j$
such that ...

**22**

votes

**0**answers

472 views

### Next steps on formal proof of classification of finite simple groups

While people are steaming ahead on finessing the proof of the classification of finite simple groups (CFSG), we have a formal proof in Coq of one of the first major components: the Feit-Thompson ...